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.
is rewritten by a rewrite rule based on the lemma
and the variable z in the lemma is bound to a term s by the match of C against t, then the subgoal which has to be proven for the rewrite rule to be valid is
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.