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
|
Module Ltac1.
Notation "& [ , x ; y ; .. ; z ]" :=
(match cons x (cons y .. (cons z nil) ..) return True with xs => ltac:(exact I) end)
(only parsing).
Check &[ , 0 ; 1 ].
End Ltac1.
Module Ltac1Fail.
Notation "& [ , x ; y ; .. ; z ]" :=
(match cons x (cons y .. (cons z nil) ..) return True with xs => ltac:(exact y) end)
(only parsing).
Fail Check &[ , 0 ; 1 ].
End Ltac1Fail.
Require Import Ltac2.Ltac2.
Module Ltac2.
Notation "& [ , x ; y ; .. ; z ]" :=
(match cons x (cons y .. (cons z nil) ..) return True with xs => ltac2:(exact I) end)
(only parsing).
Check &[ , 0 ; 1 ].
End Ltac2.
Module Ltac2Fail.
(* it would be nice to error at Notation time instead of at use time
but not sure how to do that with the current design of how recursive patterns are identified *)
Notation "& [ , x ; y ; .. ; z ]" :=
(match cons x (cons y .. (cons z nil) ..) return True with xs => ltac2:(exact $preterm:y) end)
(only parsing).
Fail Check &[ , 0 ; 1 ].
End Ltac2Fail.
|
