Introduction

In Nuprl, a term is a tree data-structure. The structure of terms is explained in detail in Section . Terms have a variety of uses.

• All propositions  in Nuprl 's logic are represented as terms, as are all expressions and types in its type theory. We refer to them sometimes as object-language  terms.
• Nearly all library objects are represented as terms.

  We refer to these terms as system-language  terms.

Terms are Nuprl's equivalent of Lisp's S-expressions  ; they are used as a general-purpose uniform data-structure.

Terms are either primitive  or abstract  . Primitive terms have fixed pre-defined meanings. Abstract terms or abstractions  are defined in abstraction library objects as being equal to other terms. An abstraction is unfolded  when it is replaced by the right-hand side of its definition. Abstractions are discussed in Chapter .

The visual appearance of a term is governed by its display forms . These are defined in display-form library objects. Display forms are described in detail in Chapter .

Terms are interactively edited and viewed using a structured editor. This editor is described in Section .