diff options
| -rw-r--r-- | sec/systemt.ltx | 10 |
1 files 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} |