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