From 07269d4ab102aac0e3d4995812627d59a316d79b Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Tue, 24 Jun 2025 18:07:37 +0100
Subject: Fix 92--124.

---
 sec/systemt.ltx | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'sec/systemt.ltx')

diff --git a/sec/systemt.ltx b/sec/systemt.ltx
index a1141ab..cfcd660 100644
--- a/sec/systemt.ltx
+++ b/sec/systemt.ltx
@@ -81,12 +81,12 @@ terms are strongly normalising.
 \subsection{Strategies for Encoding Inductive Types}%
 \label{subsec:encoding-strategies}
 
-Inductive types are a useful programming abstraction that is missing from
-System~T. If we are to effectively encode an inductive type, there are three
-operations we would like to use:
+Inductive data types as found in ML are a useful programming
+abstraction that is missing from System~T. If we are to effectively
+encode a data type, there are three operations we need to account for:
 \begin{enumerate}
-  \item constructors to form values of an inductive type;
-  \item folding to fully consume an inductive value;
+  \item constructors to form values of the data type;
+  \item folding to fully consume a value;
   \item pattern matching to support iterating on multiple values simultaneously
 \end{enumerate}
 As a concrete example, consider the pseudocode in \cref{lst:tree-eq}
-- 
cgit v1.2.3

