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