nat.lam

n0 = Zero
n1 = Suc n0
n2 = Suc n1
n3 = Suc n2
n4 = Suc n3
n5 = Suc n4
n6 = Suc n5
n7 = Suc n6
n8 = Suc n7
n9 = Suc n8

n10 = mul n2 n5
n20 = mul n10 n2

add  Zero   m = m
add (Suc n) m = Suc (add n m)

sub  Zero    _	    = Zero
sub (Suc n)  Zero   = Suc n
sub (Suc n) (Suc m) = sub n m

mul  Zero   _ = Zero
mul (Suc n) m = add m (mul n m)

pow n  Zero    = n1
pow n (Suc m) = mul n (pow n m)

divSuc  Zero   _ = Zero
divSuc (Suc n) m = if (less n m) Zero (Suc (divSuc (sub n m) m))

modSuc  Zero   _ = Zero
modSuc (Suc n) m = if (less n m) (Suc n) (modSuc (sub n m) m)

div n (Suc m) = divSuc n m
mod n (Suc m) = modSuc n m

fac  Zero   = n1
fac (Suc n) = mul (Suc n) (fac n)

eq  Zero    Zero   = True
eq  Zero   (Suc _) = False
eq (Suc _)  Zero   = False
eq (Suc n) (Suc m) = eq n m

if True  = \x y -> x
if False = \x y -> y

less  Zero    Zero   = False
less  Zero   (Suc _) = True
less (Suc _)  Zero   = False
less (Suc n) (Suc m) = less n m

decimal Zero	= \x -> x
decimal (Suc n) = (decimal (div (Suc n) n10)) (digit (mod (Suc n) n10))

inc D0 = D1
inc D1 = D2
inc D2 = D3
inc D3 = D4
inc D4 = D5
inc D5 = D6
inc D6 = D7
inc D7 = D8
inc D8 = D9

digit  Zero   = D0
digit (Suc n) = inc (digit n)

main = decimal (add (fac n8) (pow n5 n6))
-- main = decimal (add (fac n6) (pow n3 n7))
-- main = decimal (fac n5)