next up previous contents index
Next: Proofs Up: The Metalanguage Previous: Tactics in ML

Basic Types in ML for Nuprl

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 gif). 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.

Richard Eaton
Thu Sep 14 08:45:18 EDT 1995