summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorChloe Brown <chloe.brown.00@outlook.com>2025-06-26 17:34:56 +0100
committerChloe Brown <chloe.brown.00@outlook.com>2025-06-26 17:34:56 +0100
commitadd6f06dcab4b83c8ed4fc3262069b5d35ae6d86 (patch)
treee51b46b41e08a87ca8bf6ff769f45b993233da56
parent2eaa70248abba984b17a422855406c28c9076bf4 (diff)
Fix 764.
-rw-r--r--sec/reducer.ltx2
1 files changed, 0 insertions, 2 deletions
diff --git a/sec/reducer.ltx b/sec/reducer.ltx
index b5edb14..af90ad0 100644
--- a/sec/reducer.ltx
+++ b/sec/reducer.ltx
@@ -11,8 +11,6 @@ steps of complete~development~\cite{cd} on a System~T term. The second
program is the encoding from \lang{} to System~T. This takes a
type-annotated \lang{} program and encodes it as a System~T term.
-\TODO{describe the syntactic sugar I have added}
-
\subsection{Fuelled System~T Reducer}%
\label{subsec:reducer}