From 6312e6ce1406cbacddae0b4ccddb9bc4c068548c Mon Sep 17 00:00:00 2001 From: Chloe Brown Date: Thu, 26 Jun 2025 18:25:20 +0100 Subject: Fix 967--979. --- sec/compiler.ltx | 18 +++++------------- 1 file changed, 5 insertions(+), 13 deletions(-) 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