Give the encoding of `snoc`.

1 files changed, 14 insertions, 2 deletions

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}