1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
|
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[ (!)] *)
|
