Commit 250a4b8b authored by Ralf Jung's avatar Ralf Jung
Browse files

rename reservation_map_alloc_update → reservation_map_alloc

parent 49f290a4
......@@ -14,7 +14,7 @@ properties of this camera are:
- The lemma [reservation_map_token_union] enables one to split [reservation_map_token]
w.r.t. disjoint union. That is, if we have [E1 ## E2], then we get
[reservation_map_token (E1 ∪ E2) = reservation_map_token E1 ⋅ reservation_map_token E2].
- The lemma [reservation_map_alloc_update] provides a frame preserving update to
- The lemma [reservation_map_alloc] provides a frame preserving update to
associate data to a key: [reservation_map_token E ~~> reservation_map_data k a]
provided [k ∈ E] and [✓ a].
......@@ -254,7 +254,7 @@ Proof.
- intros i. rewrite lookup_op lookup_empty. auto.
Qed.
Lemma reservation_map_alloc_update E k a :
Lemma reservation_map_alloc E k a :
k E a reservation_map_token E ~~> reservation_map_data k a.
Proof.
intros ??. apply cmra_total_update=> n [mf [Ef|]] //.
......
......@@ -231,7 +231,7 @@ Section gen_heap.
rewrite meta_token_eq meta_eq /meta_token_def /meta_def.
iDestruct 1 as (γm) "[Hγm Hm]". iExists γm. iFrame "Hγm".
iApply (own_update with "Hm").
apply reservation_map_alloc_update; last done.
apply reservation_map_alloc; last done.
cut (positives_flatten N @{coPset} N); first by set_solver.
rewrite nclose_eq. apply elem_coPset_suffixes.
exists 1%positive. by rewrite left_id_L.
......
Supports Markdown
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