From 84cd0255d021e5bfe0f9bd1680143287f06ba95f Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Wed, 25 Jun 2025 18:04:07 +0100
Subject: Move list operations later.

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

diff --git a/sec/encoding.ltx b/sec/encoding.ltx
index 23a8784..9b905bc 100644
--- a/sec/encoding.ltx
+++ b/sec/encoding.ltx
@@ -72,26 +72,6 @@ operator satisfies the following equation:
 \dofold{\roll*~t~u}{x}{v} \coloneq \sub{v}{x/\mapkw{}~(\lambda i. \dofold{\mathsf{index}~t~i}{x}{v})~u}
 \]
 
-We require a few operations on lists to compute this transformation:
-\begin{description}
-  \item[\(\mathsf{nil}\)] the empty list;
-  \item[\(\mathsf{cons}\)] adds an element to the head of a list;
-  \item[\(\mathsf{snoc}\)] adds an element to the tail of a list;
-  \item[\(\mathsf{length}\)] computes the number of elements in a
-    list; and
-  \item[\(\mathsf{index}\)] retrieves a value from a list by position.
-\end{description}
-
-We give the equations these operators satisfy below.
-\begin{align*}
-\mathsf{snoc}~\mathsf{nil}~v &= \mathsf{cons}~v~\mathsf{nil} &
-\mathsf{snoc}~(\mathsf{cons}~t~u)~v &= \mathsf{cons}~t~(\mathsf{snoc}~u~v) \\
-\mathsf{length}~\mathsf{nil} &= \zero &
-\mathsf{length}~(\mathsf{cons}~t~u) &= \suc~(\mathsf{length}~u) \\
-\mathsf{index}~(\mathsf{cons}~t~u)~\zero &= t &
-\mathsf{index}~(\mathsf{cons}~t~u)~(\suc~n) &= \mathsf{index}~u~n
-\end{align*}
-
 To encode \roll{} into \roll*{} we require a function that traverses a
 value of type \(\sub{A}{X/\mu X. A}\) and collects all inductive
 components into a single list.  We can extend a list with a single
@@ -117,6 +97,26 @@ that calls each accumulator within \(A\) in sequence.  The definition
 is by induction on the well-formedness derivation of \(A\). The
 details of the definition are in \cref{M-sec:distrib}.
 
+We require a few operations on lists to compute this transformation:
+\begin{description}
+  \item[\(\mathsf{nil}\)] the empty list;
+  \item[\(\mathsf{cons}\)] adds an element to the head of a list;
+  \item[\(\mathsf{snoc}\)] adds an element to the tail of a list;
+  \item[\(\mathsf{length}\)] computes the number of elements in a
+    list; and
+  \item[\(\mathsf{index}\)] retrieves a value from a list by position.
+\end{description}
+
+We give the equations these operators satisfy below.
+\begin{align*}
+\mathsf{snoc}~\mathsf{nil}~v &= \mathsf{cons}~v~\mathsf{nil} &
+\mathsf{snoc}~(\mathsf{cons}~t~u)~v &= \mathsf{cons}~t~(\mathsf{snoc}~u~v) \\
+\mathsf{length}~\mathsf{nil} &= \zero &
+\mathsf{length}~(\mathsf{cons}~t~u) &= \suc~(\mathsf{length}~u) \\
+\mathsf{index}~(\mathsf{cons}~t~u)~\zero &= t &
+\mathsf{index}~(\mathsf{cons}~t~u)~(\suc~n) &= \mathsf{index}~u~n
+\end{align*}
+
 At the end of this phase, the \systemtinline{compose} example is
 unchanged. The \systemtinline{balanced} example reduces to the below
 code. Notice how the \suc{} branch uses the same variable
-- 
cgit v1.2.3