
----
---- 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
