From e3ad4a67050c8e918afeb069f40d88f5a4e7b21a Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Thu, 26 Jun 2025 18:18:27 +0100
Subject: Fix 941--947.

---
 sec/compiler.ltx | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'sec/compiler.ltx')

diff --git a/sec/compiler.ltx b/sec/compiler.ltx
index f7a53b3..e8c1664 100644
--- a/sec/compiler.ltx
+++ b/sec/compiler.ltx
@@ -38,10 +38,10 @@ staged compiler for expressions using MetaML~\cite{metaml}. The
 interpreter only reports errors about the combinators at run time.
 
 We adapted the combinator interpreter for Idris 2. First, we used
-dependant types to statically enforce a combinator is well-formed. The
-``parse'' interpretation function requires a certificate that a parser
-is well-formed. Second, our interpreter produces a certificate that
-the list of unprocessed tokens is a suffix of the input tokens. This
+dependant types to statically enforce a combinator is well-formed; the
+interpretation function takes a certificate that a parser is
+well-formed. Second, our interpreter produces a certificate that the
+list of unprocessed tokens is a suffix of the input tokens. This
 certificate is required to satisfy the Idris termination checker when
 interpreting fixed point combinators. Finally, we thread state
 throughout the combinators.
-- 
cgit v1.2.3

