diff options
| -rw-r--r-- | sec/encoding.ltx | 23 |
1 files changed, 8 insertions, 15 deletions
diff --git a/sec/encoding.ltx b/sec/encoding.ltx index 4d1ce74..e7dfd96 100644 --- a/sec/encoding.ltx +++ b/sec/encoding.ltx @@ -23,11 +23,11 @@ of seven phases are: \end{enumerate} We will give two running examples throughout, both with regards to the -binary tree type \(\mu X. (\nat \to \nat) + X \times X\), where leaves labelled -by functions from natural to natural. In our first example we -construct a balanced binary tree of depth \(n + 1\), with leaves -filled by \systemtinline{f}. This will demonstrate how we encode -constructors for inductive types. +binary tree type \TODO{type syntax: \(\mu X. (\nat \to \nat) + X \times X\)}, +where leaves are labelled by unary functions on naturals. In our first +example we construct a balanced binary tree of depth \(n + 1\), +filling leaves with a given function \systemtinline{f}. This will +demonstrate how we encode constructors for inductive types. \begin{listing}[H] \begin{systemt} let balanced n f = primrec n with @@ -37,16 +37,9 @@ let balanced n f = primrec n with \vspace{-\baselineskip} \end{listing} -Our other example composes the leaves of a tree into a single function, -starting by applying the right-most leaf to the input value. This will -show how we encode destructors for inductive types. -\begin{listing}[H] -\begin{systemt} -let compose tree = foldmatch tree with - Leaf f => f -| Branch (f, g) => fun x => f (g x) -\end{systemt} -\end{listing} +We will also use the \systemtinline{compose} function given in the +introduction. This will show how we encode destructors for inductive +types. \subsection{Phase 1: Simplifying Roll}% \label{subsec:simplify-roll} |