From 2d033819b2666f92e90a91d8284768097fa0ee79 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Tue, 29 Apr 2025 17:51:46 +0100
Subject: Move figure before reference.

---
 sec/encoding.ltx | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'sec/encoding.ltx')

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
-- 
cgit v1.2.3