From 0b053008c566f1666a9ff765255fe0e09dcd85a3 Mon Sep 17 00:00:00 2001
From: jihgfee <jihgfee@gmail.com>
Date: Mon, 26 Oct 2020 16:11:17 +0100
Subject: [PATCH] Made another lemma syntactically equivalent to paper
presentation
---
theories/examples/list_rev.v | 3 +--
1 file changed, 1 insertion(+), 2 deletions(-)
diff --git a/theories/examples/list_rev.v b/theories/examples/list_rev.v
index 676c718..e499654 100644
--- a/theories/examples/list_rev.v
+++ b/theories/examples/list_rev.v
@@ -62,8 +62,7 @@ Section list_rev_example.
iIntros (l xs) "Hl".
iDestruct (llist_split with "Hl") as (vs) "[Hl HIT]".
iExists l, vs. iFrame "Hl".
- iModIntro.
- iIntros "Hl".
+ iModIntro. iIntros "Hl".
iSplitL "Hl HIT".
{ iApply llist_split. rewrite big_sepL2_reverse_2.
iExists (reverse vs). iFrame "Hl HIT". }
--
GitLab