next up previous contents index
Next: Shortcuts in the Up: The Rules Previous: Optional Parameters and

Hidden Assumptions

For certain rules, we need to be able to control the free variables occuring in the extract term. The mechanism used to achieve this is that of hidden hypotheses. A hypothesis is hidden when it is displayed enclosed in square brackets. At the moment the only place where such hypotheses are added is in a subgoal of the set  elim rule. The intended meaning of a hypothesis being hidden is that the name of the hypothesis cannot appear free in the extracted term; that is, that it cannot be used computationally. Accordingly, a hidden hypothesis cannot be the object of an elim or hyp rule. For the rules for which the extract term is the trivial term axiom, the extract term contains no free variable references and so all restrictions on the use of hidden  hypotheses can be removed. The editor will remove the brackets from any hidden hypotheses in displaying a goal of this form.

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