Commit 85b06738 authored by Ralf Jung's avatar Ralf Jung

doc introduction for ownp

parent cceb5c12
...@@ -5,6 +5,15 @@ From iris.algebra Require Import auth. ...@@ -5,6 +5,15 @@ From iris.algebra Require Import auth.
From iris.proofmode Require Import tactics classes. From iris.proofmode Require Import tactics classes.
Set Default Proof Using "Type". Set Default Proof Using "Type".
(**
This module provides an interface to handling ownership of the global state that
works more like Iris 2.0 did. The state interpretation (in WP) is fixed to be
authoritative ownership of the entire state (using the [excl] RA). Users can
then put the corresponding fragment into an invariant on their own to establish
a more interesting notion of ownership, such as the standard heap with disjoint
union.
*)
Class ownPG (Λ : language) (Σ : gFunctors) := OwnPG { Class ownPG (Λ : language) (Σ : gFunctors) := OwnPG {
ownP_invG : invG Σ; ownP_invG : invG Σ;
ownP_inG :> inG Σ (authR (optionUR (exclR (stateC Λ)))); ownP_inG :> inG Σ (authR (optionUR (exclR (stateC Λ))));
......
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