diff options
Diffstat (limited to 'test-suite/output/Notations2.v')
| -rw-r--r-- | test-suite/output/Notations2.v | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/test-suite/output/Notations2.v b/test-suite/output/Notations2.v index e902a3c2..e53c94ef 100644 --- a/test-suite/output/Notations2.v +++ b/test-suite/output/Notations2.v @@ -25,6 +25,11 @@ Remove Printing Let prod. Check match (0,0,0) with (x,y,z) => x+y+z end. Check let '(a,b,c) := ((2,3),4) in a. +(* Check printing of notations with mixed reserved binders (see bug #2571) *) + +Implicit Type myx : bool. +Check exists myx y, myx = y. + (* Test notation for anonymous functions up to eta-expansion *) Check fun P:nat->nat->Prop => fun x:nat => ex (P x). @@ -83,3 +88,13 @@ Notation "'mylet' f [ x ; .. ; y ] := t 'in' u":= Check mylet f [x;y;z;(a:bool)] := x+y+z+1 in f 0 1 2. *) + +(* Check notations for functional terms which do not necessarily + depend on their parameter *) +(* Old request mentioned again on coq-club 20/1/2012 *) + +Notation "# x : T => t" := (fun x : T => t) + (at level 0, t at level 200, x ident). + +Check # x : nat => x. +Check # _ : nat => 2. |