Commit f11955d6 authored by Robbert Krebbers's avatar Robbert Krebbers

Fix typos in the documentation of program_logic/model.

parent 46087950
Pipeline #2587 passed with stage
in 4 minutes and 14 seconds
......@@ -5,7 +5,7 @@ From iris.algebra Require cofe_solver.
(** In this file we construct the type [iProp] of propositions of the Iris
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:
......@@ -44,7 +44,7 @@ Coercion gFunctors_lookup : gFunctors >-> Funclass.
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 :=
iprodURF (λ i, gmapURF gname (Σ 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