Commit fb3145be authored by Jonas Kastberg Hinrichsen's avatar Jonas Kastberg Hinrichsen
Browse files

minor changes

parent f2534449
......@@ -223,7 +223,15 @@ Section gen_proc.
iModIntro. rewrite to_gen_proc_insert. repeat rewrite insert_insert. rewrite to_gen_proc_insert. rewrite to_gen_heap_insert. unfold proc_match. unfold to_gen_heap. rewrite fmap_insert. rewrite fmap_empty. iFrame.
Qed.
Lemma gen_proc_dealloc (p:L) (l:L) (v:V) (σ:gmap L (gmap L V)) :
(* Lemma gen_proc_dealloc (p:L) (σ:gmap L (gmap L V)) : *)
(* gen_proc_ctx σ -∗ p↦{ p } ==∗ gen_proc_ctx (delete p σ). *)
(* Proof. *)
(* iIntros "Hσ Hl". rewrite /gen_proc_ctx mapsto_eq /mapsto_def. *)
(* rewrite to_gen_proc_delete. iApply (own_update_2 with "Hσ Hl"). *)
(* eapply auth_update_dealloc, (delete_singleton_local_update _ _ _). *)
(* Qed. *)
Lemma gen_proc_dealloc_val (p:L) (l:L) (v:V) (σ:gmap L (gmap L V)) :
gen_proc_ctx σ - l p{p} v == gen_proc_ctx (delete2 p l σ) ( p{ p } ).
Proof.
iIntros "Hσ Hl".
......
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