diff options
Diffstat (limited to 'test-suite/output/Notations.v')
-rw-r--r-- | test-suite/output/Notations.v | 23 |
1 files changed, 23 insertions, 0 deletions
diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v new file mode 100644 index 000000000..deb3bb078 --- /dev/null +++ b/test-suite/output/Notations.v @@ -0,0 +1,23 @@ +(* 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. + |