From 4912a660db1af2822a147eb647ca8034e8ae7173 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 10 Dec 2017 14:05:30 +0100
Subject: [PATCH] Docs: fix references to Banach.
---
docs/model.tex | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/docs/model.tex b/docs/model.tex
index a241fdad7..9d1bef1a0 100644
--- a/docs/model.tex
+++ b/docs/model.tex
@@ -80,7 +80,7 @@ For every definition, we have to show all the side-conditions: The maps have to
\Sem{\vctx \proves \term(\termB) : \type'}_\gamma &\eqdef
\Sem{\vctx \proves \term : \type \to \type'}_\gamma(\Sem{\vctx \proves \termB : \type}_\gamma) \\
\Sem{\vctx \proves \MU \var:\type. \term : \type}_\gamma &\eqdef
- \mathit{fix}(\Lam \termB : \Sem{\type}. \Sem{\vctx, x : \type \proves \term : \type}_{\mapinsert \var \termB \gamma}) \\
+ \fixp_{\Sem{\type}}(\Lam \termB : \Sem{\type}. \Sem{\vctx, x : \type \proves \term : \type}_{\mapinsert \var \termB \gamma}) \\
~\\
\Sem{\vctx \proves \textlog{abort}\;\term : \type}_\gamma &\eqdef \mathit{abort}_{\Sem\type}(\Sem{\vctx \proves \term:0}_\gamma) \\
\Sem{\vctx \proves () : 1}_\gamma &\eqdef () \\
@@ -102,7 +102,7 @@ For every definition, we have to show all the side-conditions: The maps have to
An environment $\vctx$ is interpreted as the set of
finite partial functions $\rho$, with $\dom(\rho) = \dom(\vctx)$ and
$\rho(x)\in\Sem{\vctx(x)}$.
-Above, $\mathit{fix}$ is the fixed-point on COFEs, and $\mathit{abort}_T$ is the unique function $\emptyset \to T$.
+Above, $\fixp$ is Banach's fixed-point (see \thmref{thm:banach}), and $\mathit{abort}_T$ is the unique function $\emptyset \to T$.
\paragraph{Logical entailment.}
We can now define \emph{semantic} logical entailment.
--
GitLab