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)])