Агда на окнах: `→` не в области видимости - PullRequest
Новая
       17

Агда на окнах: `→` не в области видимости

3 голосов
/ 17 мая 2019

Я пытаюсь запустить главу 1 из Основы языка программирования в Agda на компьютере с Windows.

Это свежая установка Agda 2.5.2 и Emacs 25.1.1 из MSI и нетронутый код Agda из учебника.

Я получаю эту ошибку: 

Not in scope:
  → at C:\bb\plfa.github.io\src\plfa\Naturals.lagda:51,14-17
when scope checking →

Когда я запускаю agda в командной строке, яполучите похожее сообщение об ошибке, на этот раз с правильно отображенным символом →: 

Checking plfa.Naturals (C:\bb\plfa.github.io\src\plfa\Naturals.lagda).
C:\bb\plfa.github.io\src\plfa\Naturals.lagda:51,14-17
Not in scope:
  → at C:\bb\plfa.github.io\src\plfa\Naturals.lagda:51,14-17
when scope checking →

Строка, на которую жалуется Агда, является последней в этом блоке кода: 

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ
\end{code}

Тот же код отлично работает в Ubuntu.

Я подтвердил, что символ правильный: я получаю тот же результат, если удаляю его и набираю \to.

1 Ответ

0 голосов
/ 19 мая 2019

Есть ли у вас похожие проблемы при компиляции других файлов, не связанных с PLFA?Это больше похоже на проблему Агды, чем на проблему ЛЖВС.Если это не так, я могу порекомендовать попробовать Agda 2.5.4.2, которая является текущей минимальной версией для PLFA (см. https://plfa.github.io/GettingStarted/)

...