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
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
|
[<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]
fun f : forall x : bool * (nat * unit), ?T =>
CURRYINV (x : nat) (y : bool), f
: (forall x : bool * (nat * unit), ?T) ->
forall (x : nat) (y : bool), ?T@{x:=(y, (x, tt))}
where
?T : [x : bool * (nat * unit) |- Type]
fun f : forall x : unit * nat * bool, ?T => CURRYLEFT (x : nat) (y : bool), f
: (forall x : unit * nat * bool, ?T) ->
forall (x : nat) (y : bool), ?T@{x:=(tt, x, y)}
where
?T : [x : unit * nat * bool |- Type]
fun f : forall x : unit * bool * nat, ?T =>
CURRYINVLEFT (x : nat) (y : bool), f
: (forall x : unit * bool * nat, ?T) ->
forall (x : nat) (y : bool), ?T@{x:=(tt, y, x)}
where
?T : [x : unit * bool * nat |- Type]
forall n : nat, {#n | 1 > n}
: Prop
forall x : nat, {|x | x > 0|}
: Prop
exists2 x : nat, x = 1 & x = 2
: Prop
fun n : nat =>
foo2 n (fun x y z : nat => (fun _ _ _ : nat => x + y + z = 0) z y x)
: nat -> Prop
fun n : nat =>
foo2 n (fun a b c : nat => (fun _ _ _ : nat => a + b + c = 0) c b a)
: nat -> Prop
fun n : nat =>
foo2 n (fun n0 y z : nat => (fun _ _ _ : nat => n0 + y + z = 0) z y n0)
: nat -> Prop
fun n : nat =>
foo2 n (fun x n0 z : nat => (fun _ _ _ : nat => x + n0 + z = 0) z n0 x)
: nat -> Prop
fun n : nat =>
foo2 n (fun x y n0 : nat => (fun _ _ _ : nat => x + y + n0 = 0) n0 y x)
: nat -> Prop
fun n : nat => {|n, y | fun _ _ _ : nat => n + y = 0 |}_2
: nat -> Prop
fun n : nat => {|n, y | fun _ _ _ : nat => n + y = 0 |}_2
: nat -> Prop
fun n : nat => {|n, n0 | fun _ _ _ : nat => n + n0 = 0 |}_2
: nat -> Prop
fun n : nat =>
foo2 n (fun x y z : nat => (fun _ _ _ : nat => x + y + n = 0) z y x)
: nat -> Prop
fun n : nat =>
foo2 n (fun x y z : nat => (fun _ _ _ : nat => x + y + n = 0) z y x)
: nat -> Prop
fun n : nat => {|n, fun _ : nat => 0 = 0 |}_3
: nat -> Prop
fun n : nat => {|n, fun _ : nat => n = 0 |}_3
: nat -> Prop
fun n : nat => foo3 n (fun x _ : nat => ETA z : nat, (fun _ : nat => x = 0))
: nat -> Prop
fun n : nat => {|n, fun _ : nat => 0 = 0 |}_4
: nat -> Prop
fun n : nat => {|n, fun _ : nat => n = 0 |}_4
: nat -> Prop
fun n : nat => foo4 n (fun _ _ : nat => ETA z : nat, (fun _ : nat => z = 0))
: nat -> Prop
fun n : nat => foo4 n (fun _ y : nat => ETA z : nat, (fun _ : nat => y = 0))
: nat -> Prop
tele (t : Type) '(y, z) (x : t0) := tt
: forall t : Type, nat * nat -> t -> fpack
[fun x : nat => x + 0;; fun x : nat => x + 1;; fun x : nat => x + 2]
: (nat -> nat) *
((nat -> nat) *
((nat -> nat) *
((nat -> nat) * ((nat -> nat) * ((nat -> nat) * (nat -> nat))))))
foo5 x nat x
: nat -> nat
fun x : ?A => x === x
: forall x : ?A, x = x
where
?A : [x : ?A |- Type] (x cannot be used)
|
