Commit 4ac784a4 authored by Robbert Krebbers's avatar Robbert Krebbers

Remove wrong comment.

parent ec399a74
......@@ -6,8 +6,7 @@ Definition memcpy : val := λ: "arg",
"n" ←ᶜ a_ret (Snd (Snd "arg"));
"pend" ←ᶜ ∗ᶜ (a_ret "p") +∗ᶜ (a_ret "n");
while (∗ᶜ (a_ret "p") <∗ᶜ a_ret "pend") {
(a_ret "p" += 1) = ∗ᶜ(a_ret "q" += 1);
skip (* sequence point, should be implicit in the def. of while *)
(a_ret "p" += 1) = ∗ᶜ(a_ret "q" += 1)
}.
Lemma memcpy_spec `{amonadG Σ} lxs lys xs ys n R :
......
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