(* Natural Numbers *)

(* 
 * First encoding. Try evaluating zero'.succ, zero'.succ.pred, etc. 
 *)
zero' = [iszero = true,
        pred = @(x)x,
        succ = @(x)(x.iszero := false).pred := x];

(*  
 * Second encoding. Try evaluating iszero(zero), iszero(one).
 *)
zero = [case = \(z)\(s)z,
        succ = @(x) x.case := \(z)\(s)s(x)];
one  = zero.succ;
two  = one.succ;

iszero = \(n)n.case(true)(\(p)false);
pred   = \(n)n.case(zero)(\(p)p);