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.