From a3e1369fae5befbc61499f83cee093dd1f4a290f Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Thu, 22 May 2025 12:55:47 +0100
Subject: Describe high-level algorithm.

---
 sec/reducer.ltx | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'sec/reducer.ltx')

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
-- 
cgit v1.2.3