Commit 45b41b92 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Rename `auth_update_core_id` into `auth_update_frac_alloc`.

Also rename the recently added `view_update_alloc_frac` into
`view_update_frac_alloc` to be consistent with other lemmas about the
placement of `_frac`.
parent faa41e55
......@@ -278,10 +278,10 @@ Section auth.
exact: cmra_update_op_l.
Qed.
Lemma auth_update_core_id q a b `{!CoreId b} :
Lemma auth_update_frac_alloc q a b `{!CoreId b} :
b a {q} a ~~> {q} a b.
Proof.
intros Ha%(core_id_extract _ _). apply view_update_alloc_frac=> n bf [??].
intros Ha%(core_id_extract _ _). apply view_update_frac_alloc=> n bf [??].
split; [|done]. rewrite Ha (comm _ a). by apply cmra_monoN_l.
Qed.
......
......@@ -525,7 +525,7 @@ Section cmra.
rewrite !cmra_total_update view_validN_eq=> ?? n [[[q ag]|] bf]; naive_solver.
Qed.
Lemma view_update_alloc_frac q a b :
Lemma view_update_frac_alloc q a b :
( n bf, rel n a bf rel n a (b bf))
V{q} a ~~> V{q} a V b.
Proof.
......
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