diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-04-25 11:57:31 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-04-25 11:57:31 +0000 |
commit | 6faaf8f7bb9f14fa0f9f46c3d2e21373c9077190 (patch) | |
tree | 8284f9a09d87bb65ed7277c7e6de538d7ae25043 /test-suite/output/Notations2.out | |
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.out')
-rw-r--r-- | test-suite/output/Notations2.out | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out index 783b30c0f..2e0e145e1 100644 --- a/test-suite/output/Notations2.out +++ b/test-suite/output/Notations2.out @@ -14,6 +14,11 @@ fun (P : nat -> nat -> Prop) (x : nat) => exists x0, P x x0 : (nat -> nat -> Prop) -> nat -> Prop ∃ n p : nat, n + p = 0 : Prop +∃ x y : nat, +let b := 1 in +let c := b in +let d := 2 in ∃ z : nat, let e := 3 in let f := 4 in x + y = z + d + : Prop ∀ n p : nat, n + p = 0 : Prop λ n p : nat, n + p = 0 @@ -25,7 +30,7 @@ fun (P : nat -> nat -> Prop) (x : nat) => exists x0, P x x0 λ A : Type, ∀ n p : A, n = p : Type -> Prop Defining 'let'' as keyword -let' f (x y z : nat) (_ : bool) := x + y + z + 1 in f 0 1 2 +let' f (x y : nat) (a:=0) (z : nat) (_ : bool) := x + y + z + 1 in (f(0)) 1 2 : bool -> nat λ (f : nat -> nat) (x : nat), f(x) + S(x) : (nat -> nat) -> nat -> nat |