diff options
Diffstat (limited to 'sec/encoding.ltx')
| -rw-r--r-- | sec/encoding.ltx | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/sec/encoding.ltx b/sec/encoding.ltx index 1063ba7..bf2c96e 100644 --- a/sec/encoding.ltx +++ b/sec/encoding.ltx @@ -175,10 +175,16 @@ X)\) of countable trees. To compute the recursive depth, we need to compute the maximum of a countable sequence, which is impossible in general. Thus we cannot encode such infinite types. +Adding the \(\mathsf{snoc}\) operator may at first seem +counterproductive; we want to encode away inductive types and +recursion, yet \(\mathsf{snoc}\) is naively a recursion over an +inductive type. Fortunately there exist encodings for lists such that +not only does \(\mathsf{snoc}\) avoid recursion, but it is also as +performant as cons. + \TODO{ \begin{itemize} \item justify the head operator - \item justify the snoc operator \item justify the arb operator \end{itemize} } |