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