From 4cbf8bb52abc552a2de752f13dfc4e3bf1f9f314 Mon Sep 17 00:00:00 2001
From: jihgfee <jihgfee@gmail.com>
Date: Tue, 14 Apr 2020 12:10:20 +0200
Subject: [PATCH] Updated typing rule for chanfst

---
 theories/logrel/types.v | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

diff --git a/theories/logrel/types.v b/theories/logrel/types.v
index 87f351a..5d572fb 100644
--- a/theories/logrel/types.v
+++ b/theories/logrel/types.v
@@ -685,17 +685,18 @@ Section properties.
     Qed.
 
     Definition chanselect : val := λ: "c" "i", send "c" "i";; "c".
-    Lemma ltyped_chanselect Γ (c : val) (i : Z) (Ps : gmap Z (lsty Σ)) :
-      is_Some (Ps !! i) →
+    Lemma ltyped_chanselect Γ (c : val) (i : Z) P Ps :
+      Ps !! i = Some P →
       (Γ ⊨ c : chan (lsty_select Ps)) -∗
-      Γ ⊨ chanselect c #i : chan (Ps !!! i).
+      Γ ⊨ chanselect c #i : chan P.
     Proof.
       iIntros (Hin) "#Hc !>".
       iIntros (vs) "H /=".
       rewrite /chanselect. simpl.
       iDestruct ("Hc" with "H") as "Hc'".
       iMod (wp_value_inv with "Hc'") as "Hc'".
-      wp_send with "[]"=> //.
+      wp_send with "[]"=> //; eauto.
+      rewrite (lookup_total_correct Ps i P)=> //.
       by wp_pures.
     Qed.
 
-- 
GitLab