Coq 错误 : The reference evenb was not found in the current environment

Question

我正在尝试阅读 Software Foundations Coq 书( http://www.cis.upenn.edu/~bcpierce/sf/current/toc.html )，但是当我编译 Induction.v(看起来像 http://www.cs.uml.edu/~rhenniga/coq/sf_induction.html )时，我收到错误消息“错误:在现在的环境。” -- 即使在 Basics.v 编译之后。任何想法为什么？

Answer 1

I can confirm that opening CoqIDE from the same directory works on macOS: cd <sf-dir>; /Applications/CoqIDE_8.5.app/Contents/MacOS/coqide

来自: The reference "X" was not found in the current environment