From c6c015b92a6172b082004cae4a052f1735d83422 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Fri, 30 May 2025 15:09:12 +0100
Subject: Explain intrinsically well-scoped syntax.

---
 sec/compiler.ltx | 17 ++++++++++++++++-
 1 file changed, 16 insertions(+), 1 deletion(-)

(limited to 'sec/compiler.ltx')

diff --git a/sec/compiler.ltx b/sec/compiler.ltx
index 0948073..9be1908 100644
--- a/sec/compiler.ltx
+++ b/sec/compiler.ltx
@@ -24,12 +24,27 @@ three main components:
     guarantee it will only ever have to process well-typed terms.
 \end{itemize}
 
+We present a simplified form of the Idris types used in the compiler.
+
 \subsection{Parser}
 \TODO{
   \begin{itemize}
     \item summarise \textcite{bidir}
     \item explain dependent state
-    \item explain what intentionally well-scoped syntax is
+  \end{itemize}
+}
+
+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
+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.
+
+\TODO{
+  \begin{itemize}
     \item justify why I used intentionally well-scoped syntax
   \end{itemize}
 }
-- 
cgit v1.2.3

