The type of terms
is a recursive
data type; it is a
variant union based upon the type of term: universe, function, product, etc.
The function ` term_kind` returns the kind of the term as a token:
` `UNIVERSE``,` `FUNCTION`` or ` `PRODUCT``, for example.
Corresponding to each kind of terms is a boolean predicate: `
is_universe_term`, ` is_function_term` and ` is_product_term`,
for example.

For each kind of term there is a constructor
and a
destructor
.
For example, for universe terms the constructor, ` make_universe_term`,
maps integers (representing universe levels)
to terms.
The corresponding destructor is ` destruct_universe` and maps terms to
integers. The destructor fails if applied to a term that is not a universe
term, and the constructors for terms fail if the semantic restrictions on the
arguments are not met. For example, ` destruct_universe` fails if
applied to a nonpositive integer since it is not a legal universe level.

Nuprl defs used to construct terms are invisible to ML. Terms are, in fact, composed of two parts: an underlying term structure and a print representation. The constructors and destructors described above operate on the term structure; in the case of the constructors a reasonable print representation is calculated automatically. See below for how to examine the print representation of a term.

In addition to the individual term constructors,
constant
terms may be used
by entering any legal Nuprl
term enclosed in single quotes, as in
` 'int in U7'`. Note that these quotation marks are different
from those used for tokens in ML.

Thu Sep 14 08:45:18 EDT 1995