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.