Commit 5d81fe7a authored by Simon Friis Vindum's avatar Simon Friis Vindum Committed by Robbert Krebbers
Browse files

Apply 3 suggestion(s) to 3 file(s)

parent d8276388
......@@ -34,7 +34,7 @@ Inductive dfrac :=
(* This notation is intended to be used as a component in other notations that
include discardable fractions. The notation provides shorthands for the
constructors and the commonly used full fraction. For and example
constructors and the commonly used full fraction. For an example
demonstrating how this can be used see the notation in [gen_heap.v]. *)
Declare Custom Entry dfrac.
Notation "{ dq }" := (dq) (in custom dfrac at level 1, dq constr).
......
......@@ -185,7 +185,7 @@ Section gen_heap.
Lemma mapsto_ne l1 l2 dq2 v1 v2 : l1 v1 - l2 {dq2} v2 - l1 l2.
Proof. apply mapsto_frac_ne. intros ?%exclusive_l; [done|apply _]. Qed.
(** Permanently turn a fractional points-to predicate into a persistent
(** Permanently turn any points-to predicate into a persistent
points-to predicate. *)
Lemma mapsto_persist l dq v : l {dq} v == l ↦□ v.
Proof. rewrite mapsto_eq. apply own_update, gmap_view_persist. Qed.
......
......@@ -14,7 +14,7 @@ Class atomic_heap {Σ} `{!heapG Σ} := AtomicHeap {
store : val;
cmpxchg : val;
(* -- predicates -- *)
mapsto (l : loc) (q: dfrac) (v : val) : iProp Σ;
mapsto (l : loc) (dq: dfrac) (v : val) : iProp Σ;
(* -- mapsto properties -- *)
mapsto_timeless l q v :> Timeless (mapsto l q v);
mapsto_fractional l v :> Fractional (λ (q : Qp), mapsto l (DfracOwn q) v);
......
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