Fix 15--18.

1 files changed, 6 insertions, 4 deletions

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