Commit 02cdbd2e authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Use Lemma everywhere.

parent 96d0a8a8
......@@ -70,7 +70,7 @@ Section proof.
iApply (twp_array_free with "H"); [auto..|]; iIntros "H HΦ". by iApply "HΦ".
Qed.
Theorem twp_array_copy_to stk E (dst src : loc) vdst vsrc q (n : Z) :
Lemma twp_array_copy_to stk E (dst src : loc) vdst vsrc q (n : Z) :
Z.of_nat (length vdst) = n Z.of_nat (length vsrc) = n
[[{ dst ↦∗ vdst src ↦∗{q} vsrc }]]
array_copy_to #dst #src #n @ stk; E
......@@ -87,7 +87,7 @@ Section proof.
iIntros "[Hvdst Hvsrc]".
iApply "HΦ"; by iFrame.
Qed.
Theorem wp_array_copy_to stk E (dst src : loc) vdst vsrc q (n : Z) :
Lemma wp_array_copy_to stk E (dst src : loc) vdst vsrc q (n : Z) :
Z.of_nat (length vdst) = n Z.of_nat (length vsrc) = n
{{{ dst ↦∗ vdst src ↦∗{q} vsrc }}}
array_copy_to #dst #src #n @ stk; E
......@@ -97,7 +97,7 @@ Section proof.
iApply (twp_array_copy_to with "H"); [auto..|]; iIntros "H HΦ". by iApply "HΦ".
Qed.
Theorem twp_array_clone stk E l q vl n :
Lemma twp_array_clone stk E l q vl n :
Z.of_nat (length vl) = n
(0 < n)%Z
[[{ l ↦∗{q} vl }]]
......@@ -114,7 +114,7 @@ Section proof.
wp_pures.
iApply "HΦ"; by iFrame.
Qed.
Theorem wp_array_clone stk E l q vl n :
Lemma wp_array_clone stk E l q vl n :
Z.of_nat (length vl) = n
(0 < n)%Z
{{{ l ↦∗{q} vl }}}
......
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