gulcii-0.3: lib/church.gu

id = \x . x
const = \x y . x
true = \t f . t
false = \t f . f
and = \a b . a b a
or = \a b . a a b
not = \a . a false true
zero = \s z . z
succ = \n s z . s (n s z)
iszero = \n . n (const false) true
add = \m n . m succ n
mul = \m n . m (add n) zero
exp = \m n . n m
pred = \n s z . n (\g h . h (g s)) (\u . z) (\u . u)
sub = \m n . n pred m
equal = \m n . and (iszero (sub m n)) (iszero (sub n m))
nil = \c n . n
cons = \x xs c n . c x (xs c n)
isnil = \l . l (\x xs . false) true
head = \l . l (\x xs . x) id
tail = \l c n . l (\x xs g . g x (xs c)) (\xs . n) (\x xs . xs)
map = \f l . l (\x xs . cons (f x) xs) nil
sum = \l . l (\x xs . add x xs) zero
length = \l . l (\x xs . succ xs) zero
pair = \a b p . p a b
fst = \p . p (\a b . a)
snd = \p . p (\a b . b)
nothing = \n j . n
just = \a n j . j a
maybe = \n j m . m n j
left = \a l r . l a
right = \b l r . r b
either = \l r e . e l r