在当前环境中找不到引用 "X"
The reference "X" was not found in the current environment
我正在使用 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 的重复，因为我已经做了那些事情：
编译Basics.v。检查 Basics.vo 是否在目录中。现在编译Induction.v。最后一步失败。
我自己也遇到过这个错误。尝试从 Software Foundations 文件所在的同一目录打开 CoqIDE，然后从那里编译。如果您在 Linux 上，只需打开一个终端，转到该目录，然后在其中键入 coqide。我不太清楚如何在其他系统上执行此操作，例如Mac OS，但我确实注意到，仅通过图标打开应用程序会使它失败。
我正在使用 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 的重复，因为我已经做了那些事情：
编译Basics.v。检查 Basics.vo 是否在目录中。现在编译Induction.v。最后一步失败。
我自己也遇到过这个错误。尝试从 Software Foundations 文件所在的同一目录打开 CoqIDE，然后从那里编译。如果您在 Linux 上，只需打开一个终端，转到该目录，然后在其中键入 coqide。我不太清楚如何在其他系统上执行此操作，例如Mac OS，但我确实注意到，仅通过图标打开应用程序会使它失败。