Commit e2407f9f authored by Ralf Jung's avatar Ralf Jung
Browse files

heap_lang lifting: instantiate inv_heapG and inv_heap_inv

parent 6dba682d
......@@ -204,7 +204,7 @@ Section tests.
End tests.
Section notation_tests.
Context `{!heapG Σ, inv_heapG loc val Σ}.
Context `{!heapG Σ, !inv_heapG Σ}.
(* Make sure these parse and type-check. *)
Lemma inv_mapsto_own_test (l : loc) : l _(λ _, True) #5. Abort.
From stdpp Require Import fin_maps.
From iris.proofmode Require Import tactics.
From iris.algebra Require Import auth gmap.
From iris.base_logic.lib Require Export gen_heap proph_map.
From iris.base_logic.lib Require Import gen_inv_heap.
From iris.base_logic.lib Require Export gen_heap proph_map gen_inv_heap.
From iris.program_logic Require Export weakestpre total_weakestpre.
From iris.program_logic Require Import ectx_lifting total_ectx_lifting.
From iris.heap_lang Require Export lang.
......@@ -35,6 +34,8 @@ Notation "l ↦□ I" := (inv_mapsto (L:=loc) (V:=val) l I%stdpp%type)
(at level 20, format "l ↦□ I") : bi_scope.
Notation "l ↦_ I v" := (inv_mapsto_own (L:=loc) (V:=val) l v I%stdpp%type)
(at level 20, I at level 9, format "l ↦_ I v") : bi_scope.
Notation inv_heapG := (inv_heapG loc val).
Notation inv_heap_inv := (inv_heap_inv loc val).
(** The tactic [inv_head_step] performs inversion on hypotheses of the shape
[head_step]. The tactic will discharge head-reductions starting from values, and
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