Commit 2f4811b6 authored by Ralf Jung's avatar Ralf Jung

style

parent 55294a27
......@@ -29,7 +29,7 @@ Section proof.
Definition is_lock (γ : gname) (lk : val) (R : iProp Σ) : iProp Σ :=
( l: loc, lk = #l inv N (lock_inv γ l R))%I.
Definition locked (γ : gname): iProp Σ := own γ (Excl ()).
Definition locked (γ : gname) : iProp Σ := own γ (Excl ()).
Lemma locked_exclusive (γ : gname) : locked γ - locked γ - False.
Proof. iIntros "H1 H2". by iDestruct (own_valid_2 with "H1 H2") as %?. Qed.
......
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