Coq错误：在当前环境中找不到参考evenb

我试图通过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）时，出现错误消息“错误：在当前环境中找不到参考evenb。” - 即使在编译Basics.v之后。任何想法为什么？Coq错误：在当前环境中找不到参考evenb

我们需要一些更多的上下文知道什么可能是错误的。你在使用CoqIDE吗？ Basics.v是否与Induction.v位于同一目录？编译的文件Basics.vo实际上是否显示在该目录上？ –

按照[此答案]（http://stackoverflow.com/a/16203673/596361）尝试在'Induction.v'的开头预先加入'Add LoadPath'。“'。 –

编译Basic.v与coqc Basics.v命令应生成Basic.vo和Basic.glob文件在同一目录中。那么你应该在编译Induction.v在同一个目录中也可以; coqc Induction.v。

2016-04-15 20:54:12

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

2017-06-09 10:55:16

回答