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

---
 sec/encoding.ltx | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

diff --git a/sec/encoding.ltx b/sec/encoding.ltx
index 14c6079..be049b8 100644
--- a/sec/encoding.ltx
+++ b/sec/encoding.ltx
@@ -255,10 +255,17 @@ indices, we can give an arbitrary indexing function. Recall that all
 System~T types are inhabited which allows us to construct this
 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}}\]
+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.
+
 \TODO{
   \begin{itemize}
     \item explain why a list is a pair of length and index function
-    \item give the encoding of cons
     \item give the encoding of snoc
     \item give the encoding of max
     \item give the encoding of head
-- 
cgit v1.2.3