Commit 5d0722f1 authored by Ike Mulder's avatar Ike Mulder
Browse files

Removed now autosolved ✓ ◯ goal.

parent a570abc2
Pipeline #64044 failed with stage
in 8 minutes and 21 seconds
......@@ -127,8 +127,6 @@ Section spec.
SPEC {{ True }}
new_lock #()
{{ (l p : loc) γe, RET #l; holds_at_loc l (is_queued_loc γe) is_queue_head γe p }}.
(* this sidecondition occurs since this approach CoAllocs an ● with a ◯, which is unusual *)
Proof. iSmash. by apply auth_frag_valid. Qed.
Global Program Instance acquire_spec (l : loc) γe :
SPEC ⟨↑N_node (p : loc), << holds_at_loc l (is_queued_loc γe) is_queue_head γe p >>
......
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