|
|
|---|
|
|
|
|---|
Fixtype of hypotheses for proof obligations.
This is a tagged union type, introduced by fty::deftagsum.
Proof obligations arise from expressions that may be contained in larger expressions. In that case, the path from the super-expression to the sub-expression may include boolean conditions (tests or negated tests) as well as bindings: these all provide hypotheses in which the proof obligation must be proved. That a boolean condition is a hypothesis is obvious. But note that also a binding can be regarded as a hypothesis of sorts, because it introduces new variables and equates them to expressions: both the new variables and the equations can be used to prove the obligation.
This fixtype captures these two kinds of hypotheses for proof obligations.