ML Constructors

One of the features of the Nuprl system is that it comes with its own formal metalanguage, implemented in ML. Accordingly, ML needs access to the rules of the system. Following is a list of the ML rule constructors. The constructors are categorized and numbered in the same manner as the rules. For example, the constructor numbered 4 in the atom section corresponds to the rule numbered 4 in the atom section. Each constructor is presented in the form constructor_name(parameter names): type. The parameter names are never actually used but appear here solely for documentation purposes. Following are some conventions regarding the parameter names which we give with their types:

• hyp:int is used to indicate a hypothesis.
• where:int is used to indicate which equand of an equality should be reduced in a computation rule.
• level:int is used to give a universe level.
• using:term is used to indicate a using term.
• over_id:tok, over:term are used to indicate an over term. If the over_id is the token `nil`, the over term is ignored.

Unlike the rules, each constructor needs a unique name. The general form of the names is base--type_ kind_ qualifier, where base--type is a prl type and kind is one of intro, elim, equality, formation or computation. So, for example, list_equality_nil is the name of the constructor for the rule which specifies how to show two nil terms are the same in a list type, and int_elim is the name of the constructor for the elim rule for integers. There are some exceptions to this general pattern, the main one being that the name of the constructor for the rule for showing two canonical type terms to be equal in some universe is type _equality rather than universe_equality_ type.