From 07269d4ab102aac0e3d4995812627d59a316d79b Mon Sep 17 00:00:00 2001 From: Chloe Brown Date: Tue, 24 Jun 2025 18:07:37 +0100 Subject: Fix 92--124. --- sec/systemt.ltx | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) 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