Forked from
Iris / Iris
Source project has a limited visibility.
-
Ralf Jung authoredThis required a new ectx axiom: Positivity of evaluation contexts. This axiom was also present in the old Iris 1.1 development, back when it still derived lifting axioms for ectx languages.
Ralf Jung authoredThis required a new ectx axiom: Positivity of evaluation contexts. This axiom was also present in the old Iris 1.1 development, back when it still derived lifting axioms for ectx languages.