summaryrefslogtreecommitdiff
path: root/sec/encoding.ltx
diff options
context:
space:
mode:
Diffstat (limited to 'sec/encoding.ltx')
-rw-r--r--sec/encoding.ltx10
1 files changed, 5 insertions, 5 deletions
diff --git a/sec/encoding.ltx b/sec/encoding.ltx
index 296bf73..8de40c4 100644
--- a/sec/encoding.ltx
+++ b/sec/encoding.ltx
@@ -138,11 +138,6 @@ this root. Instead of eagerly computing paths within the heap, we
compute new paths lazily. The only necessary value to store is the
index of the given child.
-More formally, we encode the type \(\mu X. A\) as \(\nat \times
-(\mathsf{List}~\nat \to \sub{A}{X/\nat})\), recursively encoding \(A\).
-We present the encoding of \roll*{} and \foldkw{} in
-\cref{fig:phase-2-encode}.
-
\begin{figure}
\begin{align*}
\roll*~ts~x &\coloneq \tuple*{
@@ -160,6 +155,11 @@ We present the encoding of \roll*{} and \foldkw{} in
\caption{Phase 2 encoding of the \roll*{} and \foldkw{} operators.}\label{fig:phase-2-encode}
\end{figure}
+More formally, we encode the type \(\mu X. A\) as \(\nat \times
+(\mathsf{List}~\nat \to \sub{A}{X/\nat})\), recursively encoding \(A\).
+We present the encoding of \roll*{} and \foldkw{} in
+\cref{fig:phase-2-encode}.
+
\TODO{
\begin{itemize}
\item justify the max operator