diff options
author | 2011-04-25 11:57:31 +0000 | |
---|---|---|
committer | 2011-04-25 11:57:31 +0000 | |
commit | 6faaf8f7bb9f14fa0f9f46c3d2e21373c9077190 (patch) | |
tree | 8284f9a09d87bb65ed7277c7e6de538d7ae25043 /test-suite/output/Notations2.v | |
parent | 0da6cf417bdab6d5768dad8e47e3c1ea18c1e709 (diff) |
Fixing and completing interpretation of let's in notations for iterated binders.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14060 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/output/Notations2.v')
-rw-r--r-- | test-suite/output/Notations2.v | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/test-suite/output/Notations2.v b/test-suite/output/Notations2.v index 4f9b9ccc7..e902a3c27 100644 --- a/test-suite/output/Notations2.v +++ b/test-suite/output/Notations2.v @@ -31,11 +31,13 @@ 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). @@ -57,7 +59,7 @@ 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 *) |