equal
deleted
inserted
replaced
758 \end{theorem} |
758 \end{theorem} |
759 \begin{proof} |
759 \begin{proof} |
760 Straightforward corollary of \ref{flex_blexer}. |
760 Straightforward corollary of \ref{flex_blexer}. |
761 \end{proof} |
761 \end{proof} |
762 \noindent |
762 \noindent |
|
763 To piece things together and spell out the exact correctness |
|
764 of the bitcoded lexer |
|
765 in terms of producing POSIX values, |
|
766 we use the fact from the previous chapter that |
|
767 \[ |
|
768 If \; (r, s) \rightarrow v \; then \; \lexer \; r \; s = v |
|
769 \] |
|
770 to obtain this corollary: |
|
771 \begin{corollary}\label{blexerPOSIX} |
|
772 $If \; (r, s) \rightarrow v \; then \blexer \; r \; s = v$ |
|
773 \end{corollary} |
763 Our main reason for wanting a bit-coded algorithm over |
774 Our main reason for wanting a bit-coded algorithm over |
764 the injection-based one is for its capabilities of allowing |
775 the injection-based one is for its capabilities of allowing |
765 more aggressive simplifications. |
776 more aggressive simplifications. |
766 We will elaborate on this in the next chapter. |
777 We will elaborate on this in the next chapter. |
767 |
778 |