Skip to content
Snippets Groups Projects
Commit b15d71df authored by Jonas Kastberg's avatar Jonas Kastberg
Browse files

Minor clean up

parent fe2e85d7
No related branches found
No related tags found
No related merge requests found
Pipeline #29057 passed
Hide whitespace changes
Inline Side-by-side
theories/logrel/term_typing_rules.v
+ 5
− 7
View file @ b15d71df
...@@ -57,11 +57,11 @@ Section properties. ...@@ -57,11 +57,11 @@ Section properties.
(** Basic properties *) (** Basic properties *)
Lemma ltyped_unit Γ : ⊢ Γ ⊨ #() : (). Lemma ltyped_unit Γ : ⊢ Γ ⊨ #() : ().
Proof. iIntros "!>" (vs) "Henv /=". iApply wp_value. eauto. Qed. Proof. iIntros "!>" (vs) "HΓ /=". iApply wp_value. eauto. Qed.
Lemma ltyped_bool Γ (b : bool) : ⊢ Γ ⊨ #b : lty_bool. Lemma ltyped_bool Γ (b : bool) : ⊢ Γ ⊨ #b : lty_bool.
Proof. iIntros "!>" (vs) "Henv /=". iApply wp_value. eauto. Qed. Proof. iIntros "!>" (vs) "HΓ /=". iApply wp_value. eauto. Qed.
Lemma ltyped_int Γ (i : Z) : ⊢ Γ ⊨ #i : lty_int. Lemma ltyped_int Γ (i : Z) : ⊢ Γ ⊨ #i : lty_int.
Proof. iIntros "!>" (vs) "Henv /=". iApply wp_value. eauto. Qed. Proof. iIntros "!>" (vs) "HΓ /=". iApply wp_value. eauto. Qed.
(** Arrow properties *) (** Arrow properties *)
Lemma ltyped_app Γ1 Γ2 Γ3 e1 e2 A1 A2 : Lemma ltyped_app Γ1 Γ2 Γ3 e1 e2 A1 A2 :
...@@ -481,11 +481,9 @@ Section properties. ...@@ -481,11 +481,9 @@ Section properties.
⊢ Γ ⊨ recv x : A ⫤ <[x:=(chan S)%lty]> Γ. ⊢ Γ ⊨ recv x : A ⫤ <[x:=(chan S)%lty]> Γ.
Proof. Proof.
iIntros (Hx) "!>". iIntros (vs) "HΓ"=> /=. iIntros (Hx) "!>". iIntros (vs) "HΓ"=> /=.
iDestruct (env_ltyped_lookup with "HΓ") as (v' Heq) "[Hc HΓ]". iDestruct (env_ltyped_lookup _ _ _ _ (Hx) with "HΓ") as (v' Heq) "[Hc HΓ]".
{ by apply Hx. }
rewrite Heq. rewrite Heq.
wp_recv (v) as "HA". wp_recv (v) as "HA". iFrame "HA".
iSplitL "HA"; first done.
iDestruct (env_ltyped_insert _ _ x (chan _) _ with "[Hc //] HΓ") as "HΓ"=> /=. iDestruct (env_ltyped_insert _ _ x (chan _) _ with "[Hc //] HΓ") as "HΓ"=> /=.
by rewrite insert_delete (insert_id vs). by rewrite insert_delete (insert_id vs).
Qed. Qed.
......
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