From 3f3d517d00a0d8be8c8c2559eaa9a965ffb39208 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 8 Aug 2016 11:26:01 +0200
Subject: [PATCH] Fix TODO in counter_examples.
---
program_logic/counter_examples.v | 5 ++---
1 file changed, 2 insertions(+), 3 deletions(-)
diff --git a/program_logic/counter_examples.v b/program_logic/counter_examples.v
index d1fef65e9..b539d12f6 100644
--- a/program_logic/counter_examples.v
+++ b/program_logic/counter_examples.v
@@ -156,12 +156,11 @@ Module inv. Section inv.
Proof.
iIntros "(#HsP & #HsQ & #HP)". iDestruct "HsP" as (i) "HiP".
iApply (inv_open' i). iSplit; first done.
- (* TODO: How can I state a view-shift and immediately run it? *)
- iIntros "HaP". iAssert (pvs M0 (finished γ)) with "[HaP]" as "Hf".
+ iIntros "HaP". iAssert (pvs M0 (finished γ)) with "[HaP]" as "==> Hf".
{ iDestruct "HaP" as "[Hs | [Hf _]]".
- by iApply start_finish.
- by iApply pvs_intro. }
- iVs "Hf" as "Hf". iDestruct (finished_dup with "Hf") as "[Hf Hf']".
+ iDestruct (finished_dup with "Hf") as "[Hf Hf']".
iApply pvs_intro. iSplitL "Hf'"; first by eauto.
(* Step 2: Open the Q-invariant. *)
iClear "HiP". clear i. iDestruct "HsQ" as (i) "HiQ".
--
GitLab