我正在使用 CoqIDE 完成软件基础书中关于 Coq 的练习。我可以成功编译 Basics.v,从而在我的目录中生成 Basics.vo 和 Basics.glob。当我尝试运行 Induction.v 时,它起作用了。当我尝试编译它时,它提示大量丢失的引用,例如 evenb
和 negb_involutive
.如果我将 Basics.v 内容复制到 Induction.v 中,它会编译,但显然这不是要走的路。
这不是问题 Coq error: The reference evenb was not found in the current environment 的重复,因为我已经做了这些事情:
编译基础.v.检查 Basics.vo 是否在目录中。现在编译 Induction.v。这最后一步失败了。
最佳答案
我自己也经历过这个错误。尝试从 Software Foundations 文件所在的同一目录打开 CoqIDE,然后从那里进行编译。如果您使用的是 Linux,只需打开一个终端,转到该目录,然后输入 coqide
那里。我不太知道如何在其他系统上执行此操作,例如Mac OS,但我确实注意到仅通过图标打开应用程序就会失败。
关于coq - 在当前环境中未找到引用 "X",我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/40129401/