blob: 549334b71abef228ea3e145f30acf15d5a7d886b (
plain)
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
|
(let ((False (lam (f t) f))
(True (lam (f t) t))
(If (lam (b x y) (b x y)))
(Zero (lam (z s) z))
(Succ (lam (n z s) (s n)))
(One (Succ Zero))
(Two (Succ One))
(Three (Succ Two))
(IsZero (lam (n) (n True (lam (m) False))))
(const (lam (x y) x))
(Pair (lam (a b p) (p a b)))
(fst (lam (pair) (pair (lam (a b) a))))
(snd (lam (pair) (pair (lam (a b) b))))
(fix (lam (f)
((lam (x) (f (x x)))
(lam (x) (f (x x))))))
(add (fix (lam (radd x y)
(x y (lam (n) (Succ (radd n y)))))))
(mul (fix (lam (rmul x y)
(x Zero (lam (n) (add y (rmul n y)))))))
(fac (fix (lam (rfac x)
(x
One
(lam (n) (mul x (rfac n)))))))
(eqnat (fix (lam (reqnat x y)
(x (y True (const False))
(lam (x1) (y False (lam (y1) (reqnat x1 y1))))))))
(sumto (fix (lam (rsumto n)
(n Zero
(lam (m) (add n (rsumto m)))))))
(n5 (add Two Three))
(n6 (mul Two Three))
(n17 (add n6 (add n6 n5)))
(n37 (Succ (mul n6 n6)))
(n703 (sumto n37))
(n704 (Succ (sumto n37)))
(n720 (fac n6))
)
(eqnat n720 (add n704 n17)))
|
