Skip to content

Jlo/issue12

Jørn Lode requested to merge jlo/issue12 into master

Fix issue #12 (closed).

Adds terms to Sequent.ConventionMonad (i.e. for each operation, the set of named terms in its environment [where a term is the name of an operation plus its arguments]).

constructArguments has been extended to construct the terms of the operation being applied after inferring the arguments for it.

runSequent has been extended to store (in ConventionMonad) the terms which appear in the environment of a sequent (which is later used by constructArguments above) -- at this point it will contain all the terms explicitly defined in this environment, and all terms which are in the environments of all operations used by this sequent (note the inherent transitivity -- if op3 calls op2, and op2 calls op1, then op3's environment will be made to contain all terms from op1's environment as well).

Merge request reports