diff options
author | Stephane Glondu <steph@glondu.net> | 2010-08-06 16:15:08 -0400 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2010-08-06 16:17:55 -0400 |
commit | f18e6146f4fd6ed5b8ded10a3e602f5f64f919f4 (patch) | |
tree | c413c5bb42d20daf5307634ae6402526bb994fd6 /test-suite/output/Notations2.v | |
parent | b9f47391f7f259c24119d1de0a87839e2cc5e80c (diff) |
Imported Upstream version 8.3~rc1+dfsgupstream/8.3.rc1.dfsg
Diffstat (limited to 'test-suite/output/Notations2.v')
-rw-r--r-- | test-suite/output/Notations2.v | 41 |
1 files changed, 41 insertions, 0 deletions
diff --git a/test-suite/output/Notations2.v b/test-suite/output/Notations2.v index 2e136edf..57d8ebbc 100644 --- a/test-suite/output/Notations2.v +++ b/test-suite/output/Notations2.v @@ -24,3 +24,44 @@ Check forall (A: Set) (le: A -> A -> Prop) (x y: A), le x y \/ le y x. 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. + +(* Test notations with binders *) + +Notation "∃ x .. y , P":= + (ex (fun x => .. (ex (fun y => P)) ..)) (x binder, y binder, at level 200). + +Check (∃ n p, n+p=0). + +Notation "∀ x .. y , P":= (forall x, .. (forall y, P) ..) + (x binder, at level 200, right associativity). + +Check (∀ n p, n+p=0). + +Notation "'λ' x .. y , P":= (fun x, .. (fun y, P) ..) + (y binder, at level 200, right associativity). + +Check (λ n p, n+p=0). + +Generalizable Variable A. + +Check `(λ n p : A, n=p). +Check `(∃ n p : A, n=p). +Check `(∀ n p : A, n=p). + +Notation "'let'' f x .. y := t 'in' u":= + (let f := fun x => .. (fun y => t) .. in u) + (f ident, x closed binder, y closed binder, at level 200, + right associativity). + +Check let' f x y z (a:bool) := x+y+z+1 in f 0 1 2. + +(* This one is not fully satisfactory because binders in the same type + are re-factorized and parentheses are needed even for atomic binder + +Notation "'mylet' f [ x ; .. ; y ] := t 'in' u":= + (let f := fun x => .. (fun y => t) .. in u) + (f ident, x closed binder, y closed binder, at level 200, + right associativity). + +Check mylet f [x;y;z;(a:bool)] := x+y+z+1 in f 0 1 2. +*) |