Commit 3f3d517d authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Fix TODO in counter_examples.

parent 2cb61949
......@@ -156,12 +156,11 @@ Module inv. Section inv.
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".
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment