comments

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) -∗