Commit 1c692d39 authored by Ralf Jung's avatar Ralf Jung

Fix use of undefined universe "U"

Fixes #28
parent 01e5e3f8
...@@ -152,7 +152,7 @@ The remaining domains are interpreted as follows: ...@@ -152,7 +152,7 @@ The remaining domains are interpreted as follows:
\Sem{\type \to \type'} &\eqdef& \Sem{\type} \nfn \Sem{\type} \\ \Sem{\type \to \type'} &\eqdef& \Sem{\type} \nfn \Sem{\type} \\
\end{array} \end{array}
\] \]
For the remaining base types $\type$ defined by the signature $\Sig$, we pick an object $X_\type$ in $\cal U$ and define For the remaining base types $\type$ defined by the signature $\Sig$, we pick an object $X_\type$ in $\COFEs$ and define
\[ \[
\Sem{\type} \eqdef X_\type \Sem{\type} \eqdef X_\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