From 7810bc37d75e125ecd8cb26bed6172dbf6ac065e Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 13 Aug 2019 13:28:16 +0200
Subject: [PATCH] comments

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

diff --git a/theories/heap_lang/array.v b/theories/heap_lang/array.v
index 32cd79f3b..415f1cb76 100644
--- a/theories/heap_lang/array.v
+++ b/theories/heap_lang/array.v
@@ -5,11 +5,19 @@ From iris.proofmode Require Import tactics.
 From stdpp Require Import fin_maps.
 Set Default Proof Using "Type".
 
+(** This file defines the [array] connective, a version of [mapsto] that works
+with lists of values. It also contains array versions of the basic heap
+operations of HeapLand. *)
+
 Definition array `{!heapG Σ} (l : loc) (vs : list val) : iProp Σ :=
   ([∗ list] i ↦ v ∈ vs, (l +ₗ i) ↦ v)%I.
 Notation "l ↦∗ vs" := (array l vs)
   (at level 20, format "l  ↦∗  vs") : bi_scope.
 
+(** We have no [FromSep] or [IntoSep] instances to remain forwards compatible
+with a fractional array assertion, that will split the fraction, not the
+list. *)
+
 Section lifting.
 Context `{!heapG Σ}.
 Implicit Types P Q : iProp Σ.
@@ -61,9 +69,6 @@ Proof.
   rewrite drop_insert; last by lia. done.
 Qed.
 
-(** No [FromSep] or [IntoSep] instances to remain forwards compatible with a
-fractional array assertion, that will split the fraction, not the list. *)
-
 (** Allocation *)
 Lemma mapsto_seq_array l v n :
   ([∗ list] i ∈ seq 0 n, (l +ₗ (i : nat)) ↦ v) -∗
-- 
GitLab