diff options
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 |