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
|
0
1
2
= 3
: nat
(print_id (print_id 0))
(print_id 0)
0
(print_id 0)
0
0
= print_id (print_id (print_id 0))
: nat
(print_id (print_id 0))
(print_id (print_id 0))
(print_id 0)
(print_id 0)
0
0
= 0
: nat
(1 +
(fun x : nat => print_id (1 + x) + 1)
((fun x : nat => print_id (1 + x) + 1) 0))
(1 +
(fun x : nat => print_id (1 + x) + 1)
((fun x : nat => print_id (1 + x) + 1) 0))
(1 + (fun x : nat => print_id (1 + x) + 1) 0)
(1 + (fun x : nat => print_id (1 + x) + 1) 0)
(1 + 0)
(1 + 0)
= 6
: nat
3
4
= tt
: unit
|
