Skip to content
Snippets Groups Projects
Commit 7a82a515 authored by Ralf Jung's avatar Ralf Jung
Browse files

counter_example: Turn a comment into a proper TODO

parent 0dcb2adc
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
program_logic/counter_examples.v
+ 1
− 1
View file @ 7a82a515
...@@ -156,7 +156,7 @@ Module inv. Section inv. ...@@ -156,7 +156,7 @@ Module inv. Section inv.
Proof. Proof.
iIntros "(#HsP & #HsQ & #HP)". iDestruct "HsP" as (i) "HiP". iIntros "(#HsP & #HsQ & #HP)". iDestruct "HsP" as (i) "HiP".
iApply (inv_open' i). iSplit; first done. iApply (inv_open' i). iSplit; first done.
(* Can I state a view-shift and immediately run it? *) (* 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 _]]". { iDestruct "HaP" as "[Hs | [Hf _]]".
- by iApply start_finish. - by iApply start_finish.
......
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