functions.mkd

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

Definition of functions:

A B :*
->
function :*
(f :function x :A -> apply :B)   -- application
((x :A -> y :B) ->               -- abstraction
    f :function
    (x :A -> ['apply(f,x) = 'y(x)]))

Naturals and its constructors.

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

A successor function:

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

But functions are not the typical way of working with stuff in this language, so this is just a proof of modeling power.