In specializing the ML language to Nuprl
\
we have made each of the kinds of
objects that occur in the logic into ML
base types.
The ML type proof has already been encountered. There are also types for
terms, rules and declarations (see figure 
).
These types should not be confused with types of the Nuprl
logic;
the types described here
are data types in the programming language ML that represent objects
of the logic.
Figure: Summary of the Primitive Object Language Types for ML
For each of the types there is an associated collection of predicates, constructors and destructors. The predicates on the type term, for example, allow the kind of a term to be determined. An example of a predicate on terms is is_universe_term, which returns true if and only if the term it is applied to is a universe term. The constructors
and destructors for each of the types allow new objects of the types to be synthesized and existing objects of the type to be divided into component parts. Appendix A contains a list of primitive extensions to ML that have been made in implementing tactics.