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

Merge pull request #53 from cpitclaudel/patch-1

Browse source 
Change "there exists valuation" to "there exists a valuation"
This commit is contained in:
Adam Chlipala 2021-03-16 15:49:30 -04:00 committed by GitHub
commit d86e3278c3
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
frap_book.tex
View file

@ -2032,7 +2032,7 @@ The intuition behind the rules may come best from working out an example.
\newcommand{\smallsteps}[2]{#1 \to^* #2}
\begin{theorem}
There exists valuation $v$ such that $\smallsteps{(\mupd{\mempty}{\mathtt{input}}{2}, \mathtt{factorial})}{(v, \skipe)}$ and $\msel{v}{\mathtt{output}} = 2$.
There exists a valuation $v$ such that $\smallsteps{(\mupd{\mempty}{\mathtt{input}}{2}, \mathtt{factorial})}{(v, \skipe)}$ and $\msel{v}{\mathtt{output}} = 2$.
\end{theorem}
\begin{proof}