Commit 60da0dab authored by Ralf Jung's avatar Ralf Jung

add warning about core of assertion not being non-expansive

parent c8ae55b1
......@@ -5,7 +5,14 @@ Import uPred.
(** The "core" of an assertion is its maximal persistent part.
It can be defined entirely within the logic... at least
in the shallow embedding. *)
in the shallow embedding.
WARNING: The function "coreP" is NOT NON-EXPANSIVE.
This is because the turnstile is not non-expansive as a function
from iProp to (discreteC Prop).
To obtain a core that's non-expansive, we would have to add another
modality to the logic: a box that removes access to *all* resources,
not just restricts access to the core.
*)
Definition coreP {M : ucmraT} (P : uPred M) : uPred M :=
( `(!PersistentP Q), P Q Q)%I.
......
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