summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorChloe Brown <chloe.brown.00@outlook.com>2025-06-26 18:16:14 +0100
committerChloe Brown <chloe.brown.00@outlook.com>2025-06-26 18:16:14 +0100
commitc9919add0fe4cc64021aa0fe676527199fccd245 (patch)
treeb4565be638b9f688d4a15df7d514dcc6d8ce72bd
parent02895b46ecbf12728d5545cad2361e6751c495a9 (diff)
Fix 925--927.
-rw-r--r--sec/compiler.ltx3
1 files changed, 2 insertions, 1 deletions
diff --git a/sec/compiler.ltx b/sec/compiler.ltx
index 3a3cebc..efe7cf2 100644
--- a/sec/compiler.ltx
+++ b/sec/compiler.ltx
@@ -17,7 +17,8 @@ three main components:
\item Second we perform type checking using a bidirectional
algorithm~\cite{bidir}. Along with the usual type checking result,
- the algorithm produces a runtime-erased typing derivation.
+ the algorithm produces a runtime-erased certificate that a term is
+ well/ill typed.
\item Finally we compile the term to Guile~Scheme~\cite{guile}. By
requiring an erased type derivation, the compiler can statically