diff options
Diffstat (limited to 'sec/encoding.ltx')
| -rw-r--r-- | sec/encoding.ltx | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/sec/encoding.ltx b/sec/encoding.ltx index e7dfd96..822e47a 100644 --- a/sec/encoding.ltx +++ b/sec/encoding.ltx @@ -44,14 +44,14 @@ types. \subsection{Phase 1: Simplifying Roll}% \label{subsec:simplify-roll} -Recall the typing judgement for \roll{} in \cref{fig:lang-ty}. The -argument has type \(\sub{A}{X/\mu X. A}\). One consequence of the use of -substitution is that inductive components can appear scattered -throughout a vessel of this type. Take the inductive type \(\mu -X. \lgroup (1 + \nat \times X + \mu Y. (1 + X \times Y)) \times (1 + X) \rgroup\). The -inductive parameter \(X\) appers in three seperate locations, -including within another inductive type. A vessel of this shape could -have any number of inductive components. +Recall the typing judgement for \roll{} in \cref{M-fig:lang-ty}. The +argument has type \(\sub{A}{X/\mu X. A}\). Using substitution means that +inductive components can appear scattered throughout a vessel of this +type. Take the inductive type \(\mu X. \lgroup (1 + \nat \times X + \mu Y. (1 + +X \times Y)) \times (1 + X) \rgroup\) as an example. The inductive parameter +\(X\) appears in three seperate locations, including within another +inductive type. A vessel of this shape could have any number of +inductive components. Collecting all the inductive components into one location will make future encoding steps much easier. We enforce this by removing the |