Commit 8bd17580 authored by Robbert Krebbers's avatar Robbert Krebbers

Tweak.

parent 30f4c8d0
Pipeline #16422 failed with stage
in 5 minutes and 42 seconds
......@@ -21,7 +21,7 @@ Section par_inc.
cl C #n -
CWP par_inc (cloc_to_val cl) @ R {{ v, v = #2 cl C #(2 + n) }}.
Proof.
iIntros "Hl". iApply cwp_fun.
iIntros "Hl". iApply cwp_fun; simpl.
iMod (own_alloc (! 0%nat ! 0%nat)) as (γ) "[Hγ [Hγ1 Hγ2]]"; [done|].
set (par_inc_inv := ( n' : nat, cl C #(n' + n) own γ (! n'))%I).
iApply (cwp_insert_res _ _ par_inc_inv with "[Hγ Hl]").
......
Markdown is supported
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