diff options
Diffstat (limited to 'sec')
| -rw-r--r-- | sec/encoding.ltx | 17 |
1 files changed, 6 insertions, 11 deletions
diff --git a/sec/encoding.ltx b/sec/encoding.ltx index 0c58aea..76bd922 100644 --- a/sec/encoding.ltx +++ b/sec/encoding.ltx @@ -4,17 +4,12 @@ \section{Encoding Artyst}% \label{sec:encoding} -\TODO{ - \begin{itemize} - \item remind the reader why encoding into System~T is useful - \end{itemize} -} - -There are seven phases in the encoding process. In general, each phase -removes a specific type constructor until only naturals and function -types remain. Sometimes removing types requires introducing others; -we will introduce lists and C-style unions, which we will later need -to remove. The full list of seven phases are: +We have devised an encoding of \lang{} into System~T. The encoding has +seven phases. In general, each phase removes a specific type +constructor until only naturals and function types remain. Sometimes +removing types requires introducing others; we will introduce lists +and C-style unions, which we will later need to remove. The full list +of seven phases are: \begin{enumerate} \item changing the \roll{} operator so that all inductive components are collected together in a list. |