...
 
Commits (1)
......@@ -118,7 +118,16 @@ Section proof.
wp_let. wp_bind (! _)%E.
iMod ("Hvs" with "HP") as ([xs hd]) "[[Hs Hhd] [Hvs' _]]".
wp_load. iMod ("Hvs'" with "[Hs Hhd]") as "HP"; first by iFrame.
iModIntro. wp_let. wp_alloc l as "Hl". wp_let.
iModIntro. wp_let. wp_bind (ref _)%E.
(* This works. *)
eapply tac_wp_alloc with _ "Hl" _.
let e' := match goal with |- to_val ?e' = _ => e' end in
wp_done.
Undo. Undo.
(* But this does not. *)
wp_alloc l as "Hl".
wp_let.
wp_bind (CAS _ _ _)%E.
iMod ("Hvs" with "HP") as ([xs' hd']) "[[Hs Hhd'] Hvs']".
destruct (decide (hd = hd')) as [->|Hneq].
......