From 437b0c42e713774e7a27ccdc1f08770e30aeacbd Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Thu, 19 Jun 2025 00:26:46 +0100
Subject: Fix missing character warning.

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

(limited to 'sec/compiler.ltx')

diff --git a/sec/compiler.ltx b/sec/compiler.ltx
index cd600ac..3a3cebc 100644
--- a/sec/compiler.ltx
+++ b/sec/compiler.ltx
@@ -174,12 +174,12 @@ prior computations, so we do not need to reference the raw AST.
 \Cref{fig:bidir} shows how we have modified the \lang{} typing rules
 for bidirectional type checking. The changes are
 standard~\cref{bidir}. Products can both check and synthesise types.
-The \rollkw{} operator can only be checked as there is no unique
-correct guess for the shape type. The body of a \foldkw{} must be
-checked. The induction hypothesis is added to the context, so its type
-must be known before processing the body. As the induction hypothesis
-is filled by the motive, the only mode-correct way to obtain the
-motive type is for \foldkw{} to be checked.
+The \roll{} operator can only be checked as there is no unique correct
+guess for the shape type. The body of a \foldkw{} must be checked. The
+induction hypothesis is added to the context, so its type must be
+known before processing the body. As the induction hypothesis is
+filled by the motive, the only mode-correct way to obtain the motive
+type is for \foldkw{} to be checked.
 
 The Idris~2 type for certifying the bidirectional judgement is almost
 a direct translation of the judgement in \cref{fig:bidir}. The
-- 
cgit v1.2.3

