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:
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.