This approach to partial functions has not been retained in standard Nuprl developments. See Recursive Types for supplementary material and Recursive Functions for more current practice.
For
anyone doing mathematics or programming, recursive definition
needs no motivation;
its expressiveness, elegance and computational
efficiency motivate us to
include forms of it in the Nuprl
logic.
Current work on extending the logic involves three type constructors:
rec , the inductive type constructor, permitting
inductive data types and predicates;
inf , the lazy type constructor,
permitting infinite objects;
and 
> , the partial
function space constructor,
permitting recursively defined partial functions.
This chapter gives the extensions to the system necessary for inductive types
and for partial function types;
for detailed presentations of these two types see [Constable & Mendler 85].