----
---- Lambda-calculus representation of non-negative integers
----
---- |0| = \x.x
---- |n+1| = \x.|n|
----
let zero = \x -> x
let succ = \n -> \x -> n
let pred = \n -> n zero -- when applied to 0 it returns 0.
let one = succ zero
-- is zero the identity function?
zero True
-- is one the function that given anything (False) returns the identity function?
one False True
pred one True
let two = succ one
two False False True