Почему Идрис считает, что префикс идентификатора - это ключевое слово? - PullRequest
Новая
       9

Почему Идрис считает, что префикс идентификатора - это ключевое слово?

2 голосов
/ 19 июня 2019

При попытке интерпретировать этот код 

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

я получаю ошибку 

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

, которая действительно смутила мою.Когда я пишу private поверх объявления, ошибка, похоже, исчезает, поэтому я полагаю, что эти модификаторы доступа действительно меняют способ синтаксического анализа.Однако я не понимаю, почему это должно быть.

Так почему же появляется эта ошибка?Почему синтаксический анализатор считает in ключевым словом (которое, я полагаю, является проблемой), а не частью идентификатора, если я не помещаю private непосредственно перед этим?

[EDIT]:Чтобы получить ошибку, этого кода должно быть достаточно: 

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.

1 Ответ

0 голосов
/ 21 июня 2019

Ваш код прекрасно скомпилирован для меня.Когда в прошлом у меня были not a terminator ошибки, это было почти всегда из-за некоторой ошибки отступа, которую я сделал.Но я понятия не имею, что изменится модификатор private, чтобы он работал в вашем случае.

...