我正在阅读这本书http://www.seas.upenn.edu/~cis500/current/sf/lf-current/这是对 Coq 和自动定理证明的介绍。
我首先完成了 Basics.v 文件，并在同一目录中编译它，生成 Basics.vo。然后我开始研究 Induction.v，并在引用 Basics.v 中的“evenb”函数时出错。完整的错误文本是这样的：
“当前环境中没有找到引用的evenb。”
此外，我正在使用 macOS，它无法识别命令行中的输入“coqide”。我觉得这与我最初的 coq 无法识别“evenb”引用的问题有关。以前，我只通过 IDE 而不是命令行在 Coq 中工作。任何想法如何解决这一问题？
更新
我想安装不同版本的 Coq (8.6)，因为我引用的书是专门为那个版本设计的，我觉得这可能会解决问题。如果有人对执行此操作的最佳方法有建议，请告诉我。