Commit 350f5ecf authored by Simon Hudon's avatar Simon Hudon
Browse files

Apply 1 suggestion(s) to 1 file(s)

parent 4e15875a
......@@ -206,7 +206,7 @@ Proof.
Qed.
Lemma twp_xchg_offset s E l off vs v v' :
(vs !! off) = Some v
vs !! off = Some v
val_is_unboxed v ->
[[{ l ↦∗ vs }]] Xchg #(l + off) v' @ s; E [[{ RET v; l ↦∗ <[off:=v']> vs }]].
Proof.
......
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