1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
|
2 3
: PAIR
2[+]3
: nat
forall (A : Set) (le : A -> A -> Prop) (x y : A), le x y \/ le y x
: Prop
match (0, 0, 0) with
| (x, y, z) => x + y + z
end
: nat
let '(a, _, _) := (2, 3, 4) in a
: nat
∃ n p : nat, n + p = 0
: Prop
∀ n p : nat, n + p = 0
: Prop
λ n p : nat, n + p = 0
: nat -> nat -> Prop
λ (A : Type) (n p : A), n = p
: ∀ A : Type, A -> A -> Prop
λ A : Type, ∃ n p : A, n = p
: 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
: bool -> nat
|
