Я работаю из этой книги http://www.seas.upenn.edu/~cis500/current/sf/lf-current/, которая представляет собой введение в Coq и автоматическое доказательство теорем.
Сначала я заполнил файл Basics.v и скомпилировал его в том же каталоге, создав файл Basics.vo. Затем я перешел к работе над Induction.v и получил ошибку при обращении к функции «evenb» из Basics.v. Полный текст ошибки был таким:
"Эталонная ссылка не найдена в текущей среде."
Кроме того, я работаю над macOS, и он не распознает ввод "coqide" из командной строки. Я чувствую, что это как-то связано с моей первоначальной проблемой того, что coq не распознает ссылку "evenb". Раньше я работал в Coq только через IDE, а не из командной строки. Есть идеи как это исправить?
Обновление
Я бы хотел установить другую версию Coq (8.6), поскольку книга, на которую я ссылаюсь, была разработана специально для этой версии, и я чувствую, что это может решить проблему. Если у кого-нибудь есть советы о том, как это сделать, сообщите мне.