From aa741db834a113f60159ef97a25d892d7c597c83 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Tue, 24 Jun 2025 17:46:27 +0100
Subject: Fix 15--18.

---
 sec/intro.ltx | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

(limited to 'sec/intro.ltx')

diff --git a/sec/intro.ltx b/sec/intro.ltx
index d83b19f..d586e80 100644
--- a/sec/intro.ltx
+++ b/sec/intro.ltx
@@ -11,10 +11,12 @@ the expressive power of System~T by designing a new language that
 encodes into System~T.
 
 Our language, \lang{}, adds the regular types~\cite{regular} to
-System~T. These include sums, products and some inductive types. Below
-is a small pseudocode snippet of \lang{}. The function takes a binary
-tree with leaves labelled by unary functions on naturals and outputs
-their right-to-left composition.
+System~T. These include sums, products and some inductive
+types. Whilst there are well-known techniques to encode most of these
+types in System~T, \lang{} is the first known language to do so
+automatically. Below is a small pseudocode snippet of \lang{}. The
+function takes a binary tree of unary functions and outputs their
+right-to-left composition.
 \begin{listing}[H]
   \begin{systemt}
 let compose (tree : Tree) = foldmatch tree with
-- 
cgit v1.2.3

