Move figure before reference.

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