next up previous contents index
Next: Relations Up: Rewriting Previous: Inversion Lemmas

Environments

 

An environment  is a list of propositions and declarations of variable types and that are being assumed. The environment of the conclusion of a sequent is the list of hypotheses of the sequent. The environment of a hypothesis is all the hypotheses to the left of it. We can also talk about local environments  of subterms of sequent clauses. For example, in the sequent

the local environment for subterm C of the conclusion is

The rewrite conversionals keep track of the local environment each conversion is being applied in, and every conversion takes as its first argument an e of type env which supplies this local information.

The environment information is used by conversions in three ways by the atomic lemma and hypothesis conversions.

Currently the system must be told explicitly how the environment is extended when it descends to the subterms of a term. Built in is knowledge of the , and terms. The system assumes other terms do not modify the environment, unless otherwise told by the user. see the env.ml  file for further details.



next up previous contents index
Next: Relations Up: Rewriting Previous: Inversion Lemmas



Karla Consroe
Wed Oct 23 13:48:45 EDT 1996