Skip to content
Snippets Groups Projects
Commit 348ede9f authored by Ralf Jung's avatar Ralf Jung
Browse files

Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coq

parents 1b56406c f11955d6
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 2 additions and 2 deletions
program_logic/model.v
+ 2
− 2
View file @ 348ede9f
...@@ -5,7 +5,7 @@ From iris.algebra Require cofe_solver. ...@@ -5,7 +5,7 @@ From iris.algebra Require cofe_solver.
(** In this file we construct the type [iProp] of propositions of the Iris (** In this file we construct the type [iProp] of propositions of the Iris
logic. This is done by solving the following recursive domain equation: logic. This is done by solving the following recursive domain equation:
iProp ≈ uPred { i : gid & gname -fin-> (Σ i) iProp } iProp ≈ uPred (∀ i : gid, gname -fin-> (Σ i) iProp)
where: where:
...@@ -44,7 +44,7 @@ Coercion gFunctors_lookup : gFunctors >-> Funclass. ...@@ -44,7 +44,7 @@ Coercion gFunctors_lookup : gFunctors >-> Funclass.
Definition gname := positive. Definition gname := positive.
(** The resources functor [iResF Σ A := { i : gid & gname -fin-> (Σ i) A }]. *) (** The resources functor [iResF Σ A := ∀ i : gid, gname -fin-> (Σ i) A]. *)
Definition iResF (Σ : gFunctors) : urFunctor := Definition iResF (Σ : gFunctors) : urFunctor :=
iprodURF (λ i, gmapURF gname (Σ i)). iprodURF (λ i, gmapURF gname (Σ i)).
......
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