From 95ac1a916f80ec00fc9a1588f0f5e71659ca1bd3 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Fri, 2 May 2025 16:10:47 +0100
Subject: Give the encoding of `snoc`.

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

(limited to 'sec/encoding.ltx')

diff --git a/sec/encoding.ltx b/sec/encoding.ltx
index be049b8..6574dae 100644
--- a/sec/encoding.ltx
+++ b/sec/encoding.ltx
@@ -257,16 +257,28 @@ arbitrary value.
 
 We encode \(\mathsf{cons}~t~u\), adding element \(t\) to the head of
 the list \(u\), by
-\[\tuple{\suc~u.0 , \lambda x.~\domatch{x}{\zero. t; \suc~x. {u.1}~x}}\]
+\[\tuple{\suc~u.0, \lambda x.\domatch{x}{\zero. t; \suc~x. {u.1}~x}}\]
 The length of our new list is one larger that
 the tail. To lookup a value, we first pattern match on the
 index. Index zero represents the head, which we return
 directly. Otherwise we lookup the index in the tail.
 
+The encoding of \(\mathsf{snoc}~t~u\), adding element \(u\) to the
+tail of the list \(t\), is encoded similarly:
+\[
+\tuple{
+  \suc~t.0,
+  \lambda x.\mathsf{if}~x = t.0~\mathsf{then}~u~\mathsf{else}~t.1~x
+}
+\]
+The new list is also one item longer that the old list. When looking
+up an item, we first check if the index is the last in the list. If it
+is, we return the element we are adding to the tail. Otherwise, we
+lookup the index in the old list.
+
 \TODO{
   \begin{itemize}
     \item explain why a list is a pair of length and index function
-    \item give the encoding of snoc
     \item give the encoding of max
     \item give the encoding of head
   \end{itemize}
-- 
cgit v1.2.3

