From 8f087103f85239e3f66d1bb241db7c5d3828574f Mon Sep 17 00:00:00 2001
From: jihgfee <jihgfee@gmail.com>
Date: Mon, 26 Oct 2020 16:02:55 +0100
Subject: [PATCH] Made lemma presented in paper syntactically equivalent

---
 theories/examples/basics.v | 11 +++++++----
 1 file changed, 7 insertions(+), 4 deletions(-)

diff --git a/theories/examples/basics.v b/theories/examples/basics.v
index 39aefb2..3730299 100644
--- a/theories/examples/basics.v
+++ b/theories/examples/basics.v
@@ -360,10 +360,12 @@ Proof.
     wp_pures. by iApply "HΦ".
 Qed.
 
-Lemma prog_ref_swap_loop_spec :
-  {{{ True }}} prog_ref_swap_loop #() {{{ RET #42; True }}}.
+(** This lemma is stated as the underlying weakest precondition of the
+hoare triple notation to make it equivalent to what is presented in the
+Actris journal paper *)
+Lemma prog_ref_swap_loop_spec : ∀ Φ, Φ #42 -∗ WP prog_ref_swap_loop #() {{ Φ }}.
 Proof.
-  iIntros (Φ) "_ HΦ". wp_lam.
+  iIntros (Φ) "HΦ". wp_lam.
   wp_apply (start_chan_spec prot_ref_loop); iIntros (c) "Hc".
   - iLöb as "IH". wp_lam.
     wp_recv (l x) as "Hl". wp_load. wp_store. wp_send with "[$Hl]".
@@ -371,7 +373,8 @@ Proof.
   - wp_alloc l1 as "Hl1". wp_alloc l2 as "Hl2".
     wp_send with "[$Hl1]". wp_send with "[$Hl2]".
     wp_recv as "Hl1". wp_recv as "Hl2".
-    wp_load. wp_load. wp_pures. by iApply "HΦ".
+    wp_load. wp_load.
+    wp_pures. by iApply "HΦ".
 Qed.
 
 End proofs.
-- 
GitLab