diff options
Diffstat (limited to 'sec/compiler.ltx')
| -rw-r--r-- | sec/compiler.ltx | 12 |
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 |