λ> def TRUE = \x.\y.x
Defined TRUE.
λ> def FALSE = \x.\y.y
Defined FALSE.
λ> def NOT = \p.p FALSE TRUE
Defined NOT.
λ> TRUE first second
first
λ> NOT TRUE
(\x.(\y.y)) # FALSE as defined.
λ> def ZERO = \f.\x.x
Defined ZERO.
λ> def SUCC = \n.\f.\x.f (n f x)
Defined SUCC.
λ> def TWO = SUCC (SUCC ZERO)
Defined TWO.
λ> def THREE = SUCC (SUCC (SUCC ZERO))
Defined THREE.
λ> def ADD = \m.\n.\f.\x.m f (n f x)
Defined ADD.
λ> def MULT = \m.\n.\f.m (n f)
Defined MULT.
λ> ADD TWO THREE s z
(s (s (s (s (s z))))) # five
λ> MULT TWO THREE s z
(s (s (s (s (s (s z)))))) # six