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

回答