diff options
Diffstat (limited to 'test-suite/output/Notations2.out')
| -rw-r--r-- | test-suite/output/Notations2.out | 8 |
1 files changed, 3 insertions, 5 deletions
diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out index cf45025e..58ec1de5 100644 --- a/test-suite/output/Notations2.out +++ b/test-suite/output/Notations2.out @@ -1,6 +1,6 @@ 2 3 : PAIR -2[+]3 +2 [+] 3 : nat forall (A : Set) (le : A -> A -> Prop) (x y : A), le x y \/ le y x : Prop @@ -10,7 +10,7 @@ end : nat let '(a, _, _) := (2, 3, 4) in a : nat -exists myx (y : bool), myx = y +exists myx y : bool, myx = y : Prop fun (P : nat -> nat -> Prop) (x : nat) => exists x0, P x x0 : (nat -> nat -> Prop) -> nat -> Prop @@ -24,7 +24,6 @@ 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 @@ -33,12 +32,11 @@ Identifier 'λ' now a keyword : Type -> Prop λ A : Type, ∀ n p : A, n = p : Type -> Prop -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)) +Notation plus2 n := (S(S(n))) λ n : list(nat), match n with | nil => 2 |