diff options
Diffstat (limited to 'sec')
| -rw-r--r-- | sec/encoding.ltx | 9 |
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 |