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.

• Declarations in the environment are used to infer types which help to complete matches. (See Section ).
• Environments are used to form the subgoals that have to be discharged for conditional lemma rewrites to go through. For example, if C in

  

  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

  

• The hypothesis conversions access the hyp list via environment terms.

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.