Commit 74dfa8b6 authored by Ralf Jung's avatar Ralf Jung

core comment

parent f2d12f84
...@@ -3,7 +3,9 @@ From iris.proofmode Require Import tactics. ...@@ -3,7 +3,9 @@ From iris.proofmode Require Import tactics.
Set Default Proof Using "Type". Set Default Proof Using "Type".
Import uPred. Import uPred.
(** The "core" of an assertion is its maximal persistent part. *) (** The "core" of an assertion is its maximal persistent part,
i.e. the conjunction of all persistent assertions that are weaker
than P (as in, implied by P). *)
Definition coreP {M : ucmraT} (P : uPred M) : uPred M := Definition coreP {M : ucmraT} (P : uPred M) : uPred M :=
( Q, (P Q) Q)%I. ( Q, (P Q) Q)%I.
Instance: Params (@coreP) 1. Instance: Params (@coreP) 1.
......
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