Commit 3c054eb5 authored by Robbert Krebbers's avatar Robbert Krebbers

Mapsto is timeless.

parent 53741bf7
......@@ -116,6 +116,9 @@ Section heap.
Context `{heapG Σ}.
(** General properties of mapsto *)
Global Instance heap_mapsto_timeless l q v : TimelessP (l {q} v).
Proof. rewrite /heap_mapsto. apply _. Qed.
Lemma heap_mapsto_op_eq l q1 q2 v :
(l {q1} v l {q2} v) (l {q1+q2} v).
Proof. by rewrite -auth_own_op map_op_singleton Frac_op dec_agree_idemp. Qed.
......
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