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
|
Module ClosedBinder.
Notation "'WITH' ( x1 : t1 ) , x2t2 , .. , xntn 'PRE' [ ] P 'POST' [ ] Q" :=
((fun x1 : t1 => (fun x2t2 => .. (fun xntn => (pair .. (pair x1 x2t2) .. xntn)) .. )),
(fun x1 : t1 => (fun x2t2 => .. (fun xntn => P) .. )),
(fun x1 : t1 => (fun x2t2 => .. (fun xntn => Q) .. )))
(at level 200, x1 at level 0, x2t2 closed binder, P at level 100, Q at level 100, only parsing).
Check WITH (x : nat) , (y : nat) , (z : nat) PRE [] (x, y, z) POST [] (z, y, x).
End ClosedBinder.
Module OpenBinder.
(* Not eligible as an open binder because of the separating comma *)
Fail Notation "'WITH' ( x1 : t1 ) , x2t2 , .. , xntn 'PRE' [ ] P 'POST' [ ] Q" :=
((fun x1 : t1 => (fun x2t2 => .. (fun xntn => (pair .. (pair x1 x2t2) .. xntn)) .. )),
(fun x1 : t1 => (fun x2t2 => .. (fun xntn => P) .. )),
(fun x1 : t1 => (fun x2t2 => .. (fun xntn => Q) .. )))
(at level 200, x1 at level 0, x2t2 binder, P at level 100, Q at level 100, only parsing).
End OpenBinder.
Module Constr.
Notation "'WITH' ( x1 : t1 ) , x2t2 , .. , xntn 'PRE' [ ] P 'POST' [ ] Q" :=
((fun x1 : t1 => (fun x2t2 => .. (fun xntn => (pair .. (pair x1 x2t2) .. xntn)) .. )),
(fun x1 : t1 => (fun x2t2 => .. (fun xntn => P) .. )),
(fun x1 : t1 => (fun x2t2 => .. (fun xntn => Q) .. )))
(at level 200, x1 at level 0, x2t2, P at level 100, Q at level 100, only parsing).
(* Fail because, constr used for binder defaults to name *)
Fail Check WITH (x : nat) , (y : nat) , (z : nat) PRE [] (x, y, z) POST [] (z, y, x).
End Constr.
Module ConstrAsPattern.
Notation "'WITH' ( x1 : t1 ) , x2t2 , .. , xntn 'PRE' [ ] P 'POST' [ ] Q" :=
((fun x1 : t1 => (fun x2t2 => .. (fun xntn => (pair .. (pair x1 x2t2) .. xntn)) .. )),
(fun x1 : t1 => (fun x2t2 => .. (fun xntn => P) .. )),
(fun x1 : t1 => (fun x2t2 => .. (fun xntn => Q) .. )))
(at level 200, x1 at level 0, x2t2 constr as pattern, P at level 100, Q at level 100, only parsing).
Check WITH (x : nat) , (y : nat) , (z : nat) PRE [] (x, y, z) POST [] (z, y, x).
End ConstrAsPattern.
Module Pattern.
Notation "'WITH' ( x1 : t1 ) , x2t2 , .. , xntn 'PRE' [ ] P 'POST' [ ] Q" :=
((fun x1 : t1 => (fun x2t2 => .. (fun xntn => (pair .. (pair x1 x2t2) .. xntn)) .. )),
(fun x1 : t1 => (fun x2t2 => .. (fun xntn => P) .. )),
(fun x1 : t1 => (fun x2t2 => .. (fun xntn => Q) .. )))
(at level 200, x1 at level 0, x2t2 pattern, P at level 100, Q at level 100, only parsing).
Check WITH (x : nat) , (y : nat) , (z : nat) PRE [] (x, y, z) POST [] (z, y, x).
End Pattern.
Module OnlyRecursiveBinderPartOfIssue17904.
Notation "∀ x .. y , P" := (forall x , .. (forall y , P) .. )
(at level 200, x constr at level 8 as pattern, right associativity,
format "'[ ' '[ ' ∀ x .. y ']' , '/' P ']'") : type_scope.
Check ∀ a b, a + b = 0.
End OnlyRecursiveBinderPartOfIssue17904.
|
