Primitive Recursive Functions

Since primitive  recursive function objects are not available in Nuprl , they have to be simulated. Consider the primitive recursive function

Shown below is a DEF that serves as a template for defining such functions.

    (F such that F(0,y)=(<G:base>)(y),
                 F(n+1,y)=(<H:body>)(n,F(n,y),y)
    )
    ==
    \n.(\y.ind(n;
               u,v."?";
               (\_y_.(<G>)(_y_));
               u,v.(\_y_.(<H>)(u)(v(_y_))(_y_))
              )
              (y) 
       )

The DEF above could be used to define an exponentiation DEF in the following way.

    <y:int>**<n:int>
    ==
    ((F such that F(0,y)=(\z.z)(y),
                  F(n+1,y)=(\a.\b.\c.(b*c))(n,F(n,y),y)
     )(<n>)
    )(<y>)