Commit b7536bf7 authored by Giuseppe Castagna's avatar Giuseppe Castagna
Browse files

typo

parent 91a1fc2d
......@@ -316,7 +316,7 @@ Ergo $t_1\setminus (t_2^+\to
\neg t)$ removes, among others, all functions in $t_1$ that diverge on $t_2^+$.
Let us see all this on our example \eqref{exptre}, in particular, by showing how this technique deduces that the type of $x_1$ in the positive branch is (a subtype of) $\Int{\vee}\String\to\Int$.
Take the static type of $x_1$, that is $(\Int{\vee}\String\to\Int)\vee(\Bool{\vee}\String\to\Bool)$ and intersect it with
$(t_2^+\to \neg t)$, that is, $\String\to\neg\Int$. Since intersection distributes over unions we
$\lnot(t_2^+\to \neg t)$, that is, $\neg(\String\to\neg\Int)$. Since intersection distributes over unions we
obtain
\svvspace{-1mm}
%
......
......@@ -984,7 +984,10 @@ times at this point, please define it.
\end{answer}
\item
p5,11, `intersect it with': Surely the next term $(t^+ \to\neg t)$ should be negated.
p5,11, `intersect it with': Surely the next term $(t_2^+ \to\neg t)$ should be negated.
\begin{answer}
Indeed, thanks. Done.
\end{answer}
\item
p7,44, typo: `andjump'
......
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