next up previous contents index
Next: Declarations Up: Basic Types in Previous: Proofs


The rule  

constructors in ML do not correspond precisely to the rules in Nuprl . Refinement rules in are usually entered as `` intro'', `` elim'', `` hyp'', etc. Strictly speaking, the notation `` intro'' refers not to a single refinement rule but to a collection of introduction refinement rules, and the context of the proof is used to disambiguate the intended introduction rule at the time the rule is applied to a sequent. There is a similar ambiguity with the other names of the refinement rules. In addition to this ambiguity, the various sorts of the rules require different additional arguments. For example, applying an intro rule to `` >>1 in int'' requires no further information, but applying intro to `` >>int'' requires that an integer be given. Because rules in ML may exist independently of the proof context that allows the particular kind of rule to be determined, and because functions in ML are required to have a fixed number of arguments, the rule constructors have been subdivided beyond the ambiguous classes that are normally visible to the

user. For example, there are constructors like universe_intro_integer, product_intro and function_intro, all of which are normally designated in proof editing with intro. The ML rule constructors and destructors are listed along with the inference rules in chapter 8.

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