From 6cdc0564a62249888a0e53de8d4c9387e3a421d9 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 3 Jun 2019 17:57:25 +0200
Subject: [PATCH] Update Iris documentation with functor changes.
---
docs/ghost-state.tex | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/docs/ghost-state.tex b/docs/ghost-state.tex
index b8d55d0fd..c774af107 100644
--- a/docs/ghost-state.tex
+++ b/docs/ghost-state.tex
@@ -174,7 +174,7 @@ The purpose of this section is to describe how we solve these issues.
\paragraph{Picking the resources.}
The key ingredient that we will employ on top of the base logic is to give some more fixed structure to the resources.
-To instantiate the logic with dynamic higher-order ghost state, the user picks a family of locally contractive bifunctors $(\iFunc_i : \OFEs^\op \times \OFEs \to \CMRAs)_{i \in \mathcal{I}}$.
+To instantiate the logic with dynamic higher-order ghost state, the user picks a family of locally contractive bifunctors $(\iFunc_i : \COFEs^\op \times \COFEs \to \CMRAs)_{i \in \mathcal{I}}$.
(This is in contrast to the base logic, where the user picks a single, fixed camera that has a unit.)
From this, we construct the bifunctor defining the overall resources as follows:
--
GitLab