Commit 7e1f9e05 authored by Dan Frumin's avatar Dan Frumin

Quick change

parent 8ca87cec
......@@ -23,7 +23,7 @@ Section memcpy.
qq C cloc_to_val q -
AWP while (∗ᶜ (a_ret (cloc_to_val pp)) <∗ᶜ a_ret (cloc_to_val (cloc_plus p n)))
{ (a_ret (cloc_to_val pp) += 1) = (∗ᶜ (a_ret (cloc_to_val qq) += 1)) }
@ R {{ _, p C ls2 q C ls2 }}.
@ R {{ _, p C ls2 q C ls2 pp C cloc_to_val p qq C cloc_to_val q }}.
Proof.
iIntros (Hlen1 Hlen2) "Hp Hq Hpp Hqq".
simplify_eq/=.
......
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