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[ (!)] *)