Describe the roll' operator.

1 files changed, 14 insertions, 2 deletions

diff --git a/sec/encoding.ltx b/sec/encoding.ltx
index 0e7b244..8087e20 100644
--- a/sec/encoding.ltx
+++ b/sec/encoding.ltx
@@ -60,10 +60,22 @@ inductive type \(\mu X. (1 + \nat \times X + \mu Y. 1 + X \times Y) \times (1 +
 this type can have any number of inductive values, located in distant parts of
 the term.
 
+Collecting all the inductive values into one location will make future encoding
+steps much easier. We enforce this by removing the \roll{} operator and adding
+the \roll*{} operator, which has the following type derivation:
+\[
+\begin{prooftree}
+  \hypo{\judgement{\Gamma}{t}{\mathsf{List}~(\mu X.A)}}
+  \hypo{\judgement{\Gamma}{u}{\sub{A}{X/\nat}}}
+  \infer2{\judgement{\Gamma}{\roll*~t~u}{\mu X. A}}
+\end{prooftree}
+\]
+Rather than include the inductive values within the term to roll, they are
+instead gathered into an external list. The places that contained inductive
+values in the rolled term now contain indices into the list.
+
 \TODO{
   \begin{itemize}
-    \item describe that collecting them into one location makes future encoding
-      steps easier
     \item justify why I add lists as a built-in type former
     \item describe the strength function, the key step in this phase
     \item state it is defined by induction on the outer functor