products/sources/formale sprachen/Coq/test-suite/success/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: searchabout.v   Sprache: Coq

Original von: Coq©

(** Test of the different syntaxes of SearchAbout, in particular
    with and without the [ ... ] delimiters *)

SearchAbout plus.
SearchAbout plus mult.
SearchAbout "plus_n".
SearchAbout plus "plus_n".
SearchAbout "*".
SearchAbout "*" "+".

SearchAbout plus inside Peano.
SearchAbout plus mult inside Peano.
SearchAbout "plus_n" inside Peano.
SearchAbout plus "plus_n" inside Peano.
SearchAbout "*" inside Peano.
SearchAbout "*" "+" inside Peano.

SearchAbout plus outside Peano Logic.
SearchAbout plus mult outside Peano Logic.
SearchAbout "plus_n" outside Peano Logic.
SearchAbout plus "plus_n" outside Peano Logic.
SearchAbout "*" outside Peano Logic.
SearchAbout "*" "+" outside Peano Logic.

SearchAbout -"*" "+" outside Logic.
SearchAbout -"*"%nat "+"%nat outside Logic.

SearchAbout [plus].
SearchAbout [plus mult].
SearchAbout ["plus_n"].
SearchAbout [plus "plus_n"].
SearchAbout ["*"].
SearchAbout ["*" "+"].

SearchAbout [plus] inside Peano.
SearchAbout [plus mult] inside Peano.
SearchAbout ["plus_n"] inside Peano.
SearchAbout [plus "plus_n"] inside Peano.
SearchAbout ["*"] inside Peano.
SearchAbout ["*" "+"] inside Peano.

SearchAbout [plus] outside Peano Logic.
SearchAbout [plus mult] outside Peano Logic.
SearchAbout ["plus_n"] outside Peano Logic.
SearchAbout [plus "plus_n"] outside Peano Logic.
SearchAbout ["*"] outside Peano Logic.
SearchAbout ["*" "+"] outside Peano Logic.

SearchAbout [-"*" "+"] outside Logic.
SearchAbout [-"*"%nat "+"%nat] outside Logic.


(** The example in the Reference Manual *)

Require Import ZArith.

SearchAbout Z.mul Z.add "distr".
SearchAbout "+"%Z "*"%Z "distr" -positive -Prop.
SearchAbout (?x * _ + ?x * _)%Z outside OmegaLemmas.

¤ Dauer der Verarbeitung: 0.16 Sekunden  (vorverarbeitet)  ¤



Download des
Quellennavigators
Download des
sprechenden Kalenders

in der Quellcodebibliothek suchen




Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.


Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff