-
Dan Frumin authored
A new formulation allows for doing more work inside HOSL. Γ ⊨ e ≤log≤ e' : τ <=> ∀ Δ vvs ρ, spec_ctx ρ -∗ □ ⟦ Γ ⟧* Δ vvs -∗ ⟦ τ ⟧ₑ Δ (e.[env_subst (vvs.*1)], e'.[env_subst (vvs.*2)])
775d1b06
A new formulation allows for doing more work inside HOSL. Γ ⊨ e ≤log≤ e' : τ <=> ∀ Δ vvs ρ, spec_ctx ρ -∗ □ ⟦ Γ ⟧* Δ vvs -∗ ⟦ τ ⟧ₑ Δ (e.[env_subst (vvs.*1)], e'.[env_subst (vvs.*2)])