• Ralf Jung's avatar
    Derive lifting axioms for ectx languages · 2c790e9b
    Ralf Jung authored
    This 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.
    2c790e9b
ectx_language.v 5.1 KB