Structure

A definition in a Nuprl theory for a term with opid opid usually includes the following objects in the order in which they are listed here:

• A display  form object, usually named opid _df , specifying how instances of the definition should be displayed. The right-hand-side of each clause in the display form definition shows the abstraction without any display forms. Its useful to look at this if you are confused as to the structure of a abstraction.

• An abstraction object  , usually named opid  , that specifies how the definition unfolds. You indicate to the Unfold tactic abstractions to unfold by giving the opids of the abstractions. However, the Fold tactic takes the names of the objects in which the abstractions are defined. When opid is used as the name of the abstraction object, the same name can be used for referring to an abstraction when folding and unfolding.

• A well-formedness lemma  , usually named opid_wf , that helps Nuprl type-check the definition. Occasionally there is more than one well-formedness lemma, in which case the objects are distinguished by adding suffices to opid_wf.

Sometimes there are extra ML objects and lemmas associated with a definition. Definitions are not only used for the Nuprl object language; they are also in nearly all the structures that are edited using the Nuprl editor. No well-formedness lemma is applicable in these cases.

Definitions can be set up, by creating each object in turn and editing its contents from scratch. This is a rather laborious process. The following sections describe various ML functions that can be evaluated in Nuprl's ML Top Loop to more rapidly set up new definitions.

Nuprl abstractions cannot be recursive. However, recursive definitions can be introduced by using the Y combinator  . See Section

for details.