From 6312e6ce1406cbacddae0b4ccddb9bc4c068548c Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Thu, 26 Jun 2025 18:25:20 +0100
Subject: Fix 967--979.

---
 sec/compiler.ltx | 18 +++++-------------
 1 file changed, 5 insertions(+), 13 deletions(-)

(limited to 'sec/compiler.ltx')

diff --git a/sec/compiler.ltx b/sec/compiler.ltx
index 27705b6..f1abca9 100644
--- a/sec/compiler.ltx
+++ b/sec/compiler.ltx
@@ -78,22 +78,14 @@ before the third combinator and so on.
 The parser returns an intrinsically well-scoped
 term~\cite{iwss}. Terms are a dependent data type with signature
 \verb|Context -> Type|. All variable names within a term are
-guaranteed to be bound within the context parameter or a term
+guaranteed to be bound within the context parameter or by a term
 constructor such as \letkw{} or \foldkw{}. The term is
 \emph{intrinsically} well-scoped because the binding rules are
 enforced by the term constructors; an extrinsically well-scoped term
-would use a separate predicate to prove raw syntax is well-scoped.
-
-Normally parsers produce ``raw'' abstract syntax trees with concrete
-names instead of deBruijn indices. We use dependant state to directly
-create the well-scoped AST because starting from a well-scoped AST
-simplifies the type checker.
-
-We also had the option to produce a raw AST and an extrinsic
-certificate it is well-scoped. Extrinsic certificates are best for
-certifying properties of preexisting structures. As our parser is
-creating the well-scoped AST, the raw AST cannot have been used in any
-prior computations, so we do not need to reference the raw AST.
+would use a separate predicate to prove raw syntax is well-scoped.  As
+our parser is creating the well-scoped AST, the raw AST cannot have
+been used in any prior computations, so we do not need to reference a
+raw AST.\@
 
 \subsection{Bidirectional Type Checker}
 
-- 
cgit v1.2.3

