Commit 3ba5fca8 authored by Ralf Jung's avatar Ralf Jung
Browse files

remove some inconsistent empty lines

parent ded77bc4
......@@ -228,7 +228,6 @@ Proof.
setoid_rewrite vec_to_list_insert. apply twp_xchg_offset => //.
by apply vlookup_lookup.
Qed.
Lemma wp_xchg_offset_vec s E l sz (off : fin sz) (vs : vec val sz) v :
{{{ l ↦∗ vs }}} Xchg #(l + off) v @ s; E {{{ RET (vs !!! off); l ↦∗ vinsert off v vs }}}.
Proof.
......
......@@ -323,7 +323,6 @@ Proof.
iMod (gen_heap_update with "Hσ Hl") as "[$ Hl]".
iModIntro. iSplit; first done. iSplit; first done. iFrame. by iApply "HΦ".
Qed.
Lemma wp_xchg s E l v' v :
{{{ l v' }}} Xchg (Val $ LitV (LitLoc l)) (Val v) @ s; E
{{{ RET v'; l v }}}.
......
Supports Markdown
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