Commit 51e2363b authored by Robbert Krebbers's avatar Robbert Krebbers

Move `array` out of section to avoid duplicating the notation.

parent 9f34cfe5
...@@ -32,6 +32,11 @@ Notation "l ↦{ q } -" := (∃ v, l ↦{q} v)%I ...@@ -32,6 +32,11 @@ Notation "l ↦{ q } -" := (∃ v, l ↦{q} v)%I
(at level 20, q at level 50, format "l ↦{ q } -") : bi_scope. (at level 20, q at level 50, format "l ↦{ q } -") : bi_scope.
Notation "l ↦ -" := (l {1} -)%I (at level 20) : 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 (** The tactic [inv_head_step] performs inversion on hypotheses of the shape
[head_step]. The tactic will discharge head-reductions starting from values, and [head_step]. The tactic will discharge head-reductions starting from values, and
simplifies hypothesis related to conversions from and to values, and finite map simplifies hypothesis related to conversions from and to values, and finite map
...@@ -207,12 +212,6 @@ Proof. ...@@ -207,12 +212,6 @@ Proof.
iIntros (κ v2 σ2 efs Hstep); inv_head_step. by iFrame. iIntros (κ v2 σ2 efs Hstep); inv_head_step. by iFrame.
Qed. 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. Lemma array_nil l : l ↦∗ [] emp.
Proof. by rewrite /array. Qed. Proof. by rewrite /array. Qed.
...@@ -504,6 +503,3 @@ Proof. ...@@ -504,6 +503,3 @@ Proof.
Qed. Qed.
End lifting. End lifting.
Notation "l ↦∗ vs" := (array l vs)
(at level 20, format "l ↦∗ vs") : bi_scope.
Markdown is supported
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