1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
|
let Nat = ∀(N : Type) → (N → N) → N → N
let n2 = λ(N : Type) → λ(s : N → N) → λ(z : N) → s (s z)
let n5 = λ(N : Type) → λ(s : N → N) → λ(z : N) → s (s (s (s (s z))))
let mul =
λ(a : Nat) → λ(b : Nat) → λ(N : Type) → λ(s : N → N) → λ(z : N) → a N (b N s) z
let add =
λ(a : Nat) → λ(b : Nat) → λ(N : Type) → λ(s : N → N) → λ(z : N) → a N s (b N s z)
let n10 = mul n2 n5
let n100 = mul n10 n10
let n1k = mul n10 n100
let n10k = mul n100 n100
let n100k = mul n10 n10k
let n1M = mul n10k n100
let n5M = mul n1M n5
let n10M = mul n1M n10
let n20M = mul n10M n2
in n1M Natural (λ (x:Natural) → x + 1) 0
|
