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
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
|
(**********************************************************************)
(* Notations for if and let (submitted by Roland Zumkeller) *)
Notation "a ? b ; c" := (if a then b else c) (at level 10).
Check (true ? 0 ; 1).
Check if true as x return (if x then nat else bool) then 0 else true.
Notation "'proj1' t" := (let (a,_) := t in a) (at level 1).
Check (fun e : nat * nat => proj1 e).
Notation "'decomp' a 'as' x , y 'in' b" := (let (x,y) := a in b) (at level 1).
Check (decomp (true,true) as t, u in (t,u)).
(**********************************************************************)
(* Behaviour wrt to binding variables (submitted by Roland Zumkeller) *)
Section A.
Notation "! A" := (forall _:nat, A) (at level 60).
Check ! (0=0).
Check forall n, n=0.
Check forall n:nat, 0=0.
End A.
(**********************************************************************)
(* Behaviour wrt to binding variables (cf bug report #1186) *)
Section B.
Notation "# A" := (forall n:nat, n=n->A) (at level 60).
Check forall n:nat, # (n=n).
Notation "## A" := (forall n n0:nat, n=n0->A) (at level 60).
Check forall n n0:nat, ## (n=n0).
Notation "### A" :=
(forall n n0:nat, match n with O => True | S n => n=n0 end ->A) (at level 60).
Check forall n n0:nat, ### (n=n0).
End B.
(**********************************************************************)
(* Conflict between notation and notation below coercions *)
(* Case of a printer conflict *)
Require Import BinInt.
Coercion Zpos : positive >-> Z.
Open Scope Z_scope.
(* Check that (Zpos 3) is better printed by the printer for Z than
by the printer for positive *)
Check (3 + Zpos 3).
(* Case of a num printer only below coercion (submitted by Georges Gonthier) *)
Open Scope nat_scope.
Inductive znat : Set := Zpos (n : nat) | Zneg (m : nat).
Coercion Zpos: nat >-> znat.
Delimit Scope znat_scope with znat.
Open Scope znat_scope.
Variable addz : znat -> znat -> znat.
Notation "z1 + z2" := (addz z1 z2) : znat_scope.
(* Check that "3+3", where 3 is in nat and the coercion to znat is implicit,
is printed the same way, and not "S 2 + S 2" as if numeral printing was
only tested with coercion still present *)
Check (3+3).
(**********************************************************************)
(* Check recursive notations *)
Require Import List.
Notation "[ x ; .. ; y ]" := (cons x .. (cons y nil) ..).
Check [1;2;4].
Reserved Notation "( x ; y , .. , z )" (at level 0).
Notation "( x ; y , .. , z )" := (pair .. (pair x y) .. z).
Check (1;2,4).
(* Check basic notations involving "match" *)
Section C.
Notation "'ifzero' n" := (match n with 0 => true | S _ => false end)
(at level 0, n at level 0).
Check (ifzero 3).
Notation "'pred' n" := (match n with 0 => 0 | S n' => n' end)
(at level 0, n at level 0).
Check (pred 3).
Check (fun n => match n with 0 => 0 | S n => n end).
Check (fun n => match n with S p as x => p | y => 0 end).
Notation "'ifn' x 'is' 'succ' n 'then' t 'else' u" :=
(match x with O => u | S n => t end) (at level 0, u at level 0).
Check fun x => ifn x is succ n then n else 0.
End C.
(* Check correction of bug #1179 *)
Notation "1 -" := true (at level 0).
Check 1-.
(* This is another aspect of bug #1179 (raises anomaly in 8.1) *)
Require Import ZArith.
Open Scope Z_scope.
Notation "- 4" := (-2 + -2).
Check -4.
(**********************************************************************)
(* Check notations for references with activated or deactivated *)
(* implicit arguments *)
Notation Nil := @nil.
Check Nil.
Notation NIL := nil.
Check NIL : list nat.
(**********************************************************************)
(* Test printing of notation with coercions in scope of a coercion *)
Open Scope nat_scope.
Coercion is_true := fun b => b=true.
Coercion of_nat n := match n with 0 => true | _ => false end.
Notation "'I' x" := (of_nat (S x) || true)%bool (at level 10).
Check (false && I 3)%bool /\ I 6.
(**********************************************************************)
(* Check notations with several recursive patterns *)
Open Scope Z_scope.
Notation "[| x , y , .. , z ; a , b , .. , c |]" :=
(pair (pair .. (pair x y) .. z) (pair .. (pair a b) .. c)).
Check [|1,2,3;4,5,6|].
(**********************************************************************)
(* Test recursive notations involving applications *)
(* Caveat: does not work for applied constant because constants are *)
(* classified as notations for the particular constant while this *)
(* generic application notation is classified as generic *)
Notation "{| f ; x ; .. ; y |}" := ( .. (f x) .. y).
Check fun f => {| f; 0; 1; 2 |} : Z.
|
