diff options
| -rw-r--r-- | sec/encoding.ltx | 12 |
1 files changed, 7 insertions, 5 deletions
diff --git a/sec/encoding.ltx b/sec/encoding.ltx index 6e3f362..34f3ae0 100644 --- a/sec/encoding.ltx +++ b/sec/encoding.ltx @@ -194,11 +194,13 @@ because all System~T types are inhabited. Regardless, one could prove that our encoding never calls \(\mathsf{index}\) with an out-of-bounds index. -\TODO{ - \begin{itemize} - \item justify the head operator - \end{itemize} -} +The final operator we add at this phase is \(\mathsf{match}\) on +lists. We can derive this operation using \(\mathsf{length}\) and +\(\mathsf{index}\). We can use these two operators along with +primitive recursion to define a fold over lists. With a fold, we can +implement pattern matching analagously to \unroll{}. We keep it as an +operator as our encoding of lists in the next phase will make this +more efficient. We now return to our examples. After some beta reduction we recover the following value for \systemtinline{balanced}: |