pl/frap
1
0
Fork 0
mirror of https://github.com/achlipala/frap.git synced 2024-11-10 00:07:51 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Fix two typos reported by dmz

Browse source
This commit is contained in:
Adam Chlipala 2016-05-15 14:40:57 -04:00
parent 15a5235792
commit 6dcf4c1fa7
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
frap_book.tex
View file

@ -1761,7 +1761,7 @@ As an example, consider this formalization of even-odd analysis, whose proof of
\E \; \hat{\times} \; \_ &=& \E \\
\_ \; \hat{\times} \; \E &=& \E \\
\O \; \hat{\times} \; \O &=& \O \\
\top \; \hat{\times} \; \top &=& \top \\
\_ \; \hat{\times} \; \_ &=& \top \\
\E \join \E &=& \E \\
\O \join \O &=& \O \\
\_ \join \_ &=& \top \\
@ -3099,7 +3099,7 @@ We associate this exception with \emph{program failure}, and the Hoare logic wil
The extension to program syntax is easy:
\begin{eqnarray*}
\mt{Loop} &:& \forall \alpha. \; \mt{cmd} \; \alpha
\mt{Fail} &:& \forall \alpha. \; \mt{cmd} \; \alpha
\end{eqnarray*}
That is, a failing program can be considered to return any result type, since it will never actually return normally, instead throwing an uncatchable exception.