From 50351a6bf34fa7e4980c9dfda7364a61e756e78c Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Wed, 25 Jun 2025 18:00:58 +0100
Subject: Fix 446--449.

---
 sec/encoding.ltx | 23 ++++++++++++++---------
 1 file changed, 14 insertions(+), 9 deletions(-)

diff --git a/sec/encoding.ltx b/sec/encoding.ltx
index 9f13f1c..23a8784 100644
--- a/sec/encoding.ltx
+++ b/sec/encoding.ltx
@@ -73,17 +73,22 @@ operator satisfies the following equation:
 \]
 
 We require a few operations on lists to compute this transformation:
-\(\mathsf{nil}\) representing the empty list; \(\mathsf{cons}\) for
-adding an element to the head of a list; \(\mathsf{length}\) to
-compute a list's length; and \(\mathsf{index}\) to retrieve a value
-from a list by position. We give the four equations these operators
-satisfy below. Note that whilst this encoding phase does not strictly
-require \(\mathsf{index}\), it is both necessary to describe the
-equational theory and will be used in the next phase.
+\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{index}~(\mathsf{cons}~t~u)~\zero &= t \\
-\mathsf{length}~(\mathsf{cons}~t~u) &= \suc~(\mathsf{length}~u) &
+\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*}
 
-- 
cgit v1.2.3