From 51e2363b8ae9e6b4fe1c78b004b0b12cf754f0ed Mon Sep 17 00:00:00 2001 From: Robbert Krebbers Date: Tue, 4 Jun 2019 00:05:12 +0200 Subject: [PATCH] Move `array` out of section to avoid duplicating the notation. --- theories/heap_lang/lifting.v | 14 +++++--------- 1 file changed, 5 insertions(+), 9 deletions(-) diff --git a/theories/heap_lang/lifting.v b/theories/heap_lang/lifting.v index 262f568c..dd20b4ce 100644 --- a/theories/heap_lang/lifting.v +++ b/theories/heap_lang/lifting.v @@ -32,6 +32,11 @@ Notation "l ↦{ q } -" := (∃ v, l ↦{q} v)%I (at level 20, q at level 50, format "l ↦{ q } -") : bi_scope. Notation "l ↦ -" := (l ↦{1} -)%I (at level 20) : bi_scope. +Definition array `{!heapG Σ} (l : loc) (vs : list val) : iProp Σ := + ([∗ list] i ↦ v ∈ vs, loc_add l i ↦ v)%I. +Notation "l ↦∗ vs" := (array l vs) + (at level 20, format "l ↦∗ vs") : bi_scope. + (** The tactic [inv_head_step] performs inversion on hypotheses of the shape [head_step]. The tactic will discharge head-reductions starting from values, and simplifies hypothesis related to conversions from and to values, and finite map @@ -207,12 +212,6 @@ Proof. iIntros (κ v2 σ2 efs Hstep); inv_head_step. by iFrame. Qed. -Definition array (l : loc) (vs : list val) : iProp Σ := - ([∗ list] i ↦ v ∈ vs, loc_add l i ↦ v)%I. - -Notation "l ↦∗ vs" := (array l vs) - (at level 20, format "l ↦∗ vs") : bi_scope. - Lemma array_nil l : l ↦∗ [] ⊣⊢ emp. Proof. by rewrite /array. Qed. @@ -504,6 +503,3 @@ Proof. Qed. End lifting. - -Notation "l ↦∗ vs" := (array l vs) - (at level 20, format "l ↦∗ vs") : bi_scope. -- GitLab