From 437b0c42e713774e7a27ccdc1f08770e30aeacbd Mon Sep 17 00:00:00 2001 From: Chloe Brown 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