diff options
| -rw-r--r-- | lexer.py | 2 | ||||
| -rw-r--r-- | main.tex | 2 | ||||
| -rw-r--r-- | sec/encoding.ltx | 12 |
3 files changed, 13 insertions, 3 deletions
@@ -9,7 +9,7 @@ class SystemTLexer(OcamlLexer): aliases = ['syst'] filenames = ['*.syst'] - EXTRA_KEYWORDS = ['primrec', 'fold', 'foldmatch', 'roll'] + EXTRA_KEYWORDS = ['primrec', 'fold', 'foldmatch', 'roll', 'roll2'] def get_tokens_unprocessed(self, text): for index, token, value in OcamlLexer.get_tokens_unprocessed(self, text): @@ -247,7 +247,7 @@ %% Recursive types \ExplSyntaxOn \NewDocumentCommand \roll {s} - { \ensuremath{\mathsf{roll} \IfBooleanT{#1}{'}} } + { \ensuremath{\mathsf{roll \IfBooleanT{#1}{2}}} } \ExplSyntaxOff \newcommand\unroll{\ensuremath{\mathsf{unroll}}} \newcommand\foldkw{\ensuremath{\mathsf{fold}}} diff --git a/sec/encoding.ltx b/sec/encoding.ltx index a8d0269..6d339bd 100644 --- a/sec/encoding.ltx +++ b/sec/encoding.ltx @@ -99,7 +99,17 @@ Given a well-formedness derivation \(\jdgmnt{ty}{\Psi}{A}\), a type variable \(X \submult{A}{\sub{\alpha}{X/S \to S \times \alpha(X)}} \to S \to S \times \submult{A}{\alpha} \] that calls each accumulator within \(A\) in sequence. The definition is by -induction on the well-formedness derivation. +induction on the well-formedness derivation. At the end of this phase, the +\systemtinline{compose} example is unchanged. The \systemtinline{balanced} +example reduces to: +\begin{listing}[H] +\begin{systemt} +let balanced n f = primrec n with + Zero => roll2 [] (Leaf f) +| Suc tree => roll2 [tree, tree] (Branch (0, 1)) +\end{systemt} +\vspace{-\baselineskip} +\end{listing} \subsection{Phase 2: Encoding Inductive Types}% \label{subsec:inductive-types} |