Quelle bug_13018.v Sprache: Coq

Undelimit Scope list_scope.
Declare Custom Entry gnat.
Declare Custom Entry gargs.

Notation "!" := 42 (in custom gnat).
Notation "gargs:( e )" := e (e custom gargs).
Notation "( x )" := (cons x (@nil nat)) (in custom gargs, x custom gnat).
Notation "( x , y , .. , z )" := (cons x (cons y .. (cons z nil) ..))
(in custom gargs, x custom gnat, y custom gnat, z custom gnat).

Check gargs:( (!) ). (* cons 42 nil *)
Check gargs:( (!, !, !) ). (* cons 42 (42 :: 42 :: nil) *)

Definition OnlyGargs {T} (x:T) := x.
Notation "OnlyGargs[ x ]" := (OnlyGargs x) (at level 10, x custom gargs).
Check OnlyGargs[ (!) ]. (* OnlyGargs[ cons 42 nil] *)

Declare Custom Entry gargs999.
Notation "gargs999:( e )" := e (e custom gargs999 at level 999).
Notation "( x )" := (cons x (@nil nat)) (in custom gargs999, x custom gnat at level 999).
Notation "( x , y , .. , z )" := (cons x (cons y .. (cons z nil) ..))
(in custom gargs999, x custom gnat at level 999, y custom gnat at level 999, z custom gnat at level 999).

Check gargs999:( (!) ). (* gargs999:( (!)) *)
Check gargs999:( (!, !, !) ). (* gargs999:( (!, !, !)) *)
Check OnlyGargs[ (!) ]. (* OnlyGargs[ gargs999:( (!))] *)

Definition OnlyGargs999 {T} (x:T) := x.
Notation "OnlyGargs999[ x ]" := (OnlyGargs999 x) (at level 10, x custom gargs999 at level 999).
Check OnlyGargs999[ (!) ]. (* OnlyGargs999[ (!)] *)

quality100%

¤ Dauer der Verarbeitung: 0.4 Sekunden ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.