diff options
| -rw-r--r-- | test-suite/failure/Notations.v | 6 | ||||
| -rw-r--r-- | test-suite/output/Notations.v | 22 |
2 files changed, 28 insertions, 0 deletions
diff --git a/test-suite/failure/Notations.v b/test-suite/failure/Notations.v new file mode 100644 index 0000000000..e8ebad8fd7 --- /dev/null +++ b/test-suite/failure/Notations.v @@ -0,0 +1,6 @@ +(* Submitted by Roland Zumkeller *) + +Notation "! A" := (forall i:nat, A) (at level 60). + +(* Should fail: no dynamic capture *) +Check ! (i=i). diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v new file mode 100644 index 0000000000..e5b469dba7 --- /dev/null +++ b/test-suite/output/Notations.v @@ -0,0 +1,22 @@ +(* 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)). + +(* Submitted by Roland Zumkeller *) + +Notation "! A" := (forall _:nat, A) (at level 60). + +Check ! (0=0). +Check forall n, n=0. +Check forall n:nat, 0=0. |