为什么 Idris 认为标识符的前缀是关键字？

Question

当试图解释这段代码时

injective : {A : Type} ->
            {P : A -> Type} ->
            ((x : A) -> P x) ->
            Type

我得到了错误

   |
14 | injective : {A : Type} ->
   |           ^
not a terminator

这真的让我很困惑。当我在声明上写private 时，错误似乎消失了，所以我猜这些访问修饰符确实改变了解析的工作方式。但是，我不明白为什么会这样。

那么为什么会出现这个错误呢？如果我之前没有放置 private，为什么解析器认为 in 是关键字（我猜是问题所在）而不是标识符的一部分？

[编辑]：要得到错误，这段代码就足够了：

Subset : Type -> Type
Subset a = a -> Type

syntax [x] "in" [y] = y x

Test : Type
Test = Nat

injective : {a, b : Type} ->
            (a -> b) ->
            Type
injective {a} {b} f = (x, y : a) ->
                      f x = f y ->
                            x = y

我正在使用 Idris 1.3.1 的解释器。

Answer 1

您的代码对我来说编译得很好。当我过去遇到not a terminator 错误时，几乎总是由于我犯了一些缩进错误。但我不知道 private 修饰符会发生什么变化，以便它适用于您的情况。