functions.mkd

x :Y is shorthand for x [Y 'x].

Definition of functions:

A B :* 
->
function :*
(f :function x :A -> apply :B)
((x :A -> y :B) -> f :function)

Naturals and constructors.

nat :*
zero :nat
(x :nat -> succ :nat)

A successor function:

succF :function(nat,nat)
(x :nat -> ['apply(nat,nat,succF,x) = 'succ(x)])