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.out | |
parent | 300293c119981054c95182a90c829058530a6b6f (diff) |
Imported Upstream version 8.4~betaupstream/8.4_beta
Diffstat (limited to 'test-suite/output/Notations2.out')
-rw-r--r-- | test-suite/output/Notations2.out | 25 |
1 files changed, 23 insertions, 2 deletions
diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out index 6731d505..47741e43 100644 --- a/test-suite/output/Notations2.out +++ b/test-suite/output/Notations2.out @@ -10,10 +10,19 @@ end : nat let '(a, _, _) := (2, 3, 4) in a : nat +fun (P : nat -> nat -> Prop) (x : nat) => exists x0, P x x0 + : (nat -> nat -> Prop) -> nat -> Prop ∃ n p : nat, n + p = 0 : Prop +let a := 0 in +∃ 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 +Identifier 'λ' now a keyword λ n p : nat, n + p = 0 : nat -> nat -> Prop λ (A : Type) (n p : A), n = p @@ -22,6 +31,18 @@ let '(a, _, _) := (2, 3, 4) in a : Type -> Prop λ 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 +Identifier 'let'' now a keyword +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 +Notation plus2 n := (S (S n)) +λ n : list(nat), +match n with +| nil => 2 +| 0 :: _ => 2 +| list1 => 0 +| 1 :: _ :: _ => 2 +| plus2 _ :: _ => 2 +end + : list(nat) -> nat |