Skip to content
Snippets Groups Projects
Verified Commit 40b36618 authored by Paolo G. Giarrusso's avatar Paolo G. Giarrusso
Browse files

Export that iPreProp is a Cofe

parent 2eeebf09
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
theories/base_logic/lib/iprop.v
+ 2
− 0
View file @ 40b36618
...@@ -122,6 +122,7 @@ Module Type iProp_solution_sig. ...@@ -122,6 +122,7 @@ Module Type iProp_solution_sig.
Notation iPropI Σ := (uPredI (iResUR Σ)). Notation iPropI Σ := (uPredI (iResUR Σ)).
Notation iPropSI Σ := (uPredSI (iResUR Σ)). Notation iPropSI Σ := (uPredSI (iResUR Σ)).
Global Declare Instance iPreProp_cofe: Cofe (iPreProp Σ).
Parameter iProp_unfold: ∀ {Σ}, iProp Σ -n> iPreProp Σ. Parameter iProp_unfold: ∀ {Σ}, iProp Σ -n> iPreProp Σ.
Parameter iProp_fold: ∀ {Σ}, iPreProp Σ -n> iProp Σ. Parameter iProp_fold: ∀ {Σ}, iPreProp Σ -n> iProp Σ.
Parameter iProp_fold_unfold: ∀ {Σ} (P : iProp Σ), Parameter iProp_fold_unfold: ∀ {Σ} (P : iProp Σ),
...@@ -140,6 +141,7 @@ Module Export iProp_solution : iProp_solution_sig. ...@@ -140,6 +141,7 @@ Module Export iProp_solution : iProp_solution_sig.
ofe_funUR (λ i, gmapUR gname (Σ i (iPreProp Σ))). ofe_funUR (λ i, gmapUR gname (Σ i (iPreProp Σ))).
Notation iProp Σ := (uPredC (iResUR Σ)). Notation iProp Σ := (uPredC (iResUR Σ)).
Global Instance iPreProp_cofe: Cofe (iPreProp Σ) := _.
Definition iProp_unfold {Σ} : iProp Σ -n> iPreProp Σ := Definition iProp_unfold {Σ} : iProp Σ -n> iPreProp Σ :=
solution_fold (iProp_result Σ). solution_fold (iProp_result Σ).
Definition iProp_fold {Σ} : iPreProp Σ -n> iProp Σ := solution_unfold _. Definition iProp_fold {Σ} : iPreProp Σ -n> iProp Σ := solution_unfold _.
......
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