diff options
| -rw-r--r-- | sec/encoding.ltx | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/sec/encoding.ltx b/sec/encoding.ltx index 822e47a..9f13f1c 100644 --- a/sec/encoding.ltx +++ b/sec/encoding.ltx @@ -56,7 +56,7 @@ inductive components. Collecting all the inductive components 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: +following typing judgement. \[ \begin{prooftree} \hypo{\judgement{\Gamma}{t}{\mathsf{List}~(\mu X.A)}} @@ -65,9 +65,9 @@ following type derivation: \end{prooftree} \] Rather than including the inductive components within the argument of -\roll{}, they are instead gathered into an external list. The vessel -\(u\) now contains pointers to the inductive components within -\(t\). The new operator satisfies the following equation: +\roll{}, we instead collect them into an external list. We fill the +vessel \(u\) with pointers to the values within \(t\). The new +operator satisfies the following equation: \[ \dofold{\roll*~t~u}{x}{v} \coloneq \sub{v}{x/\mapkw{}~(\lambda i. \dofold{\mathsf{index}~t~i}{x}{v})~u} \] |