Commit a50fb42a authored by Jonas Kastberg's avatar Jonas Kastberg

Revert "Updated variable rule to be in line with paper version"

This reverts commit 03758fe2.
parent 03758fe2
Pipeline #27609 passed with stage
in 5 minutes and 44 seconds
......@@ -16,13 +16,11 @@ Section properties.
(** Variable properties *)
Lemma ltyped_var Γ (x : string) A :
<[x := A]>Γ x : A delete x Γ.
Γ !! x = Some A Γ x : A delete x Γ.
Proof.
iIntros "!>" (vs) "HΓ /=".
iDestruct (env_ltyped_lookup with "HΓ") as (v ->) "[HA HΓ]";
first by apply lookup_insert.
iApply wp_value. iFrame "HA".
by rewrite delete_insert_delete.
iIntros (HΓx) "!>"; iIntros (vs) "HΓ /=".
iDestruct (env_ltyped_lookup with "HΓ") as (v ->) "[HA HΓ]"; first done.
iApply wp_value. eauto with iFrame.
Qed.
(** Subtyping *)
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment