Commit 4526e514 authored by Robbert Krebbers's avatar Robbert Krebbers

Docs: fixpoints only exist when the type is inhabited.

parent c22e7b33
Pipeline #6509 passed with stages
in 15 minutes and 33 seconds
......@@ -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}
}
......
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