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
28
29
30
31
32
33
34
|
[<0, 2 >]
: nat * nat * (nat * nat)
[<0, 2 >]
: nat * nat * (nat * nat)
(0, 2, (2, 2))
: nat * nat * (nat * nat)
pair (pair O (S (S O))) (pair (S (S O)) O)
: prod (prod nat nat) (prod nat nat)
<< 0, 2, 4 >>
: nat * nat * nat * (nat * (nat * nat))
<< 0, 2, 4 >>
: nat * nat * nat * (nat * (nat * nat))
(0, 2, 4, (2, (2, 0)))
: nat * nat * nat * (nat * (nat * nat))
(0, 2, 4, (0, (2, 4)))
: nat * nat * nat * (nat * (nat * nat))
pair (pair (pair O (S (S O))) (S (S (S (S O)))))
(pair (S (S (S (S O)))) (pair (S (S O)) O))
: prod (prod (prod nat nat) nat) (prod nat (prod nat nat))
ETA x y : nat, Nat.add
: nat -> nat -> nat
ETA x y : nat, Nat.add
: nat -> nat -> nat
ETA x y : nat, Nat.add
: nat -> nat -> nat
fun x y : nat => Nat.add x y
: forall (_ : nat) (_ : nat), nat
ETA x y : nat, le_S
: forall x y : nat, x <= y -> x <= S y
fun f : forall x : nat * (bool * unit), ?T => CURRY (x : nat) (y : bool), f
: (forall x : nat * (bool * unit), ?T) ->
forall (x : nat) (y : bool), ?T@{x:=(x, (y, tt))}
where
?T : [x : nat * (bool * unit) |- Type]
|
