Commit d8e78bef authored by Hai Dang's avatar Hai Dang
Browse files

Remove a few TODOs

parent f20de0eb
......@@ -749,7 +749,6 @@ Lemma AtomicPtsTo_AtomicCASer_agree_2 l γ ζ ζ' m :
AtomicPtsTo l γ ζ m - l cas{γ,1} ζ' - ⌜ζ' = ζ⌝.
Proof. apply view_at_wand_lr, AtomicPtsTo_AtomicCASer_agree. Qed.
(* TODO: subjectively embed *)
Lemma AtomicCASer_AtomicSeen_join_l_obj l γ ζ q V :
@{V} l cas{γ,q} ζ - l sn{γ} ζ - l cas{γ,q} ζ.
Proof.
......@@ -885,7 +884,6 @@ Proof.
- iExists tx. by iFrame.
Qed.
(* TODO: can SGS be a cmra transformer? Is this related to auth's view? *)
Lemma AtomicPtsTo_CAS_to_SW l γ ζ ζ' V0:
@{V0} l cas{γ} ζ - l cas{γ,1} ζ' - l sy{γ} ζ'
== @{V0} l sw{γ} ζ l sw{γ} ζ.
......
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