Describe high-level algorithm.

1 files changed, 8 insertions, 0 deletions

diff --git a/sec/reducer.ltx b/sec/reducer.ltx
index a781a0c..2eaca08 100644
--- a/sec/reducer.ltx
+++ b/sec/reducer.ltx
@@ -129,6 +129,14 @@ let step (t : Term) : Term =
 \subsection{Encoding Algorithm}%
 \label{subsec:encoding}
 
+In \cref{M-sec:encoding} we described a process to embed \lang{}
+within System~T. We have written this algorithm in \lang{} itself,
+simultaneously mechanising the conversion and proving it is
+terminating. Our input is type-annotated \lang{} terms, and we output
+unannotated System~T terms as in \cref{lst:term-ty}. Each phase is
+accompanied by its own inductive types representing types and
+type-annotated terms.
+
 \TODO{
   \begin{itemize}
     \item describe the inputs to the embedding