Documentation

Church-encoded Nat as a PLC type.

all (r :: *). r -> (r -> r) -> r

Church-encoded '0' as a PLC term.

/\(r :: *) -> \(z : r) (f : r -> r) -> z

Church-encoded succ as a PLC term.

\(n : nat) -> /\(r :: *) -> \(z : r) (f : r -> r) -> f (n {r} z f)