Commit dc0db6aa authored by Gaurav Parthasarathy's avatar Gaurav Parthasarathy

simplified new_rdcss

parent 606e1571
Pipeline #18188 failed with stage
......@@ -28,13 +28,9 @@ Set Default Proof Using "Type".
*)
(*
new_rdcss(n) :=
let l_n = ref (injL n) in
l_n
new_rdcss(n) := ref (injL n)
*)
Definition new_rdcss : val :=
λ: "n",
let: "l_n" := ref (InjL "n") in "l_n".
Definition new_rdcss : val := λ: "n", ref (InjL "n").
(*
complete(l_descr, l_n) :=
......@@ -602,7 +598,6 @@ Section rdcss.
with "[Hln Hn●]") as "#InvR".
{ iNext. iDestruct "Hln" as "[Hln1 Hln2]".
iExists (Quiescent n). iFrame. }
wp_let.
iModIntro.
iApply ("HΦ" $! l_n γ_n).
iSplitR; last by iFrame. by iFrame "#".
......
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