From aa741db834a113f60159ef97a25d892d7c597c83 Mon Sep 17 00:00:00 2001 From: Chloe Brown 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