diff options
author | Stephane Glondu <steph@glondu.net> | 2012-01-12 16:02:20 +0100 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2012-01-12 16:02:20 +0100 |
commit | 97fefe1fcca363a1317e066e7f4b99b9c1e9987b (patch) | |
tree | 97ec6b7d831cc5fb66328b0c63a11db1cbb2f158 /test-suite/output/Notations2.v | |
parent | 300293c119981054c95182a90c829058530a6b6f (diff) |
Imported Upstream version 8.4~betaupstream/8.4_beta
Diffstat (limited to 'test-suite/output/Notations2.v')
-rw-r--r-- | test-suite/output/Notations2.v | 26 |
1 files changed, 22 insertions, 4 deletions
diff --git a/test-suite/output/Notations2.v b/test-suite/output/Notations2.v index 57d8ebbc..e902a3c2 100644 --- a/test-suite/output/Notations2.v +++ b/test-suite/output/Notations2.v @@ -25,19 +25,25 @@ 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 notation for anonymous functions up to eta-expansion *) + +Check fun P:nat->nat->Prop => fun x:nat => ex (P x). + (* Test notations with binders *) -Notation "∃ x .. y , P":= - (ex (fun x => .. (ex (fun y => P)) ..)) (x binder, y binder, at level 200). +Notation "∃ x .. y , P":= (ex (fun x => .. (ex (fun y => P)) ..)) + (x binder, y binder, at level 200, right associativity). Check (∃ n p, n+p=0). +Check ∃ (a:=0) (x:nat) y (b:=1) (c:=b) (d:=2) z (e:=3) (f:=4), x+y = z+d. + 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) ..) +Notation "'λ' x .. y , P":= (fun x => .. (fun y => P) ..) (y binder, at level 200, right associativity). Check (λ n p, n+p=0). @@ -53,7 +59,19 @@ Notation "'let'' f x .. 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. +Check let' f x y (a:=0) z (b:bool) := x+y+z+1 in f 0 1 2. + +(* In practice, only the printing rule is used here *) +(* Note: does not work for pattern *) +Notation "f ( x )" := (f x) (at level 10, format "f ( x )"). +Check fun f x => f x + S x. + +Open Scope list_scope. +Notation list1 := (1::nil)%list. +Notation plus2 n := (S (S n)). +(* plus2 was not correctly printed in the two following tests in 8.3pl1 *) +Print plus2. +Check fun n => match n with list1 => 0 | _ => 2 end. (* This one is not fully satisfactory because binders in the same type are re-factorized and parentheses are needed even for atomic binder |