Give the encoding of `cons`.

1 files changed, 8 insertions, 1 deletions

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