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.