From 31dcef8a998341145f0b08ae25d20395eaeb9d34 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Thu, 12 Jun 2025 14:24:48 +0100
Subject: Explain why we parse to intrinsically well-scoped AST.

---
 sec/compiler.ltx | 16 ++++++++++------
 1 file changed, 10 insertions(+), 6 deletions(-)

(limited to 'sec/compiler.ltx')

diff --git a/sec/compiler.ltx b/sec/compiler.ltx
index 3f0044a..c7e161c 100644
--- a/sec/compiler.ltx
+++ b/sec/compiler.ltx
@@ -81,12 +81,16 @@ constructor such as \letkw{} or \foldkw{}. The term is
 enforced by the term constructors; an extrinsically well-scoped term
 would use a separate predicate to prove raw syntax is well-scoped.
 
-\TODO{
-  \begin{itemize}
-    \item why not raw syntax?
-    \item why not extrinsic syntax?
-  \end{itemize}
-}
+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.
 
 \subsection{Bidirectional Type Checker}
 \TODO{
-- 
cgit v1.2.3

