Fix missing character warning.

1 files changed, 6 insertions, 6 deletions

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