Skip to content

Commit

Permalink
Fix build
Browse files Browse the repository at this point in the history
  • Loading branch information
hei411 committed Jan 17, 2025
1 parent e102ca9 commit 24a2b3e
Showing 1 changed file with 2 additions and 1 deletion.
3 changes: 2 additions & 1 deletion theories/coneris/examples/random_counter3/client.v
Original file line number Diff line number Diff line change
Expand Up @@ -87,7 +87,8 @@ Section client.
{{{ ↯ (1/16) }}}
con_prog
{{{ (n:nat), RET #n; ⌜(0<n)%nat⌝ }}}.
Proof.iIntros (Φ) "Hε HΦ".
Proof.
iIntros (Φ) "Hε HΦ".
rewrite /con_prog.
wp_apply (new_counter_spec (L:=L) _ counter_nroot with "[//]") as (c) "(%γ & #Hcounter & Hfrag)".
replace (1)%Qp with (1/2+1/2)%Qp; last compute_done.
Expand Down

0 comments on commit 24a2b3e

Please sign in to comment.