From d26f21edf8e4a1f91680b56b4e5bf40d426439c3 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 4 Nov 2020 21:34:47 +0100
Subject: [PATCH] Use Lemma everywhere.

---
 theories/heap_lang/lib/array.v | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/theories/heap_lang/lib/array.v b/theories/heap_lang/lib/array.v
index cd951c052..c6c6021a4 100644
--- a/theories/heap_lang/lib/array.v
+++ b/theories/heap_lang/lib/array.v
@@ -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 }}}
-- 
GitLab