Commit 606e1571 authored by Gaurav Parthasarathy's avatar Gaurav Parthasarathy

fixed new_rdcss code description

parent 8088d25f
Pipeline #18186 canceled with stage
...@@ -29,8 +29,8 @@ Set Default Proof Using "Type". ...@@ -29,8 +29,8 @@ Set Default Proof Using "Type".
(* (*
new_rdcss(n) := new_rdcss(n) :=
let l_n = ref ( ref(injL n) ) in let l_n = ref (injL n) in
ref l_n l_n
*) *)
Definition new_rdcss : val := Definition new_rdcss : val :=
λ: "n", λ: "n",
......
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