From 821a4c23753046b7f6ff3793998daa1080bf7fa2 Mon Sep 17 00:00:00 2001
From: jihgfee <jihgfee@gmail.com>
Date: Tue, 15 Sep 2020 17:11:20 +0200
Subject: [PATCH] Whitespace cleanup
---
theories/logrel/term_typing_rules.v | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/theories/logrel/term_typing_rules.v b/theories/logrel/term_typing_rules.v
index 5108c70..75f7ef8 100644
--- a/theories/logrel/term_typing_rules.v
+++ b/theories/logrel/term_typing_rules.v
@@ -500,12 +500,12 @@ Section properties.
- wp_apply "Hv2". iApply "Hc2".
- iIntros (w1 w2) "[Hw1 Hw2]".
iSplitL "Hw1 Hw2".
- + iExists _, _. iFrame. done.
+ + iExists _, _. iFrame. done.
+ iApply "Hsplit2". iFrame "HΓ1' HΓ2'".
Qed.
End with_spawn.
-
+
Lemma ltyped_send Γ Γ' (x : string) e A S :
Γ' !! x = Some (chan (<!!> TY A; S))%lty →
(Γ ⊨ e : A ⫤ Γ') -∗
--
GitLab