diff options
Diffstat (limited to 'expr.tex')
| -rw-r--r-- | expr.tex | 6 |
1 files changed, 2 insertions, 4 deletions
@@ -28,9 +28,8 @@ The \textsf{Exp} compiler, its semantics, the compiler and the proof The Coq file is attached to this report. The report walks through the file, but occasionally discusses things out of order when this aids understandability. -The proof uses well-founded induction, which requires a library. -We also use the \textsf{Omega} library for basic arithmetic, - and the \textsf{ListNotations} module for pretty list notation. +The proof uses well-founded induction, which is most easily done with the \textsf{Wellfounded} library. +We also use \textsf{Omega} for basic arithmetic and the \textsf{ListNotations} module for pretty list notation. \coq{1}{2} @@ -125,7 +124,6 @@ Since the program is reversed for use in \textsf{pn\_eval}, we can rewrite the p \coq{76}{78} -We now consider the rest of the program. Suppose the original expression was \textsf{e = eadd e1 e2}, we now consider \textsf{pn\_eval v env ((rev (rpn v e1) ++ rev (rpn v e2)) ++ rest)} in the evaluation of \textsf{rpnadd}. |