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

- Inductive Types
- Details of the Extension
- Example Proof
- Partial Function Types
- Details of the Extension

Thu Sep 14 08:45:18 EDT 1995