From 4526e5144f2d434323bca59173cfe37f4941846a Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 31 Jan 2018 17:22:15 +0100
Subject: [PATCH] Docs: fixpoints only exist when the type is inhabited.
---
docs/base-logic.tex | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/docs/base-logic.tex b/docs/base-logic.tex
index 5e7d54183..450b6a6ad 100644
--- a/docs/base-logic.tex
+++ b/docs/base-logic.tex
@@ -179,7 +179,7 @@ In writing $\vctx, x:\type$, we presuppose that $x$ is not already declared in $
\infer{
\vctx, \var:\type \proves \wtt{\term}{\type} \and
\text{$\var$ is guarded in $\term$} \and
- \text{$\type$ is complete}
+ \text{$\type$ is complete and inhabited}
}{
\vctx \proves \wtt{\MU \var:\type. \term}{\type}
}
--
GitLab