参考"X"指的是"X".在当前环境中找不到 [英] The reference "X" was not found in the current environment

问题描述

我正在使用CoqIDE来完成Software Foundations一书中有关Coq的练习.我可以成功编译Basics.v，从而在我的目录中生成Basics.vo和Basics.glob.当我尝试运行Induction.v时，它可以工作.当我尝试对其进行编译时，它抱怨缺少大量引用，例如evenb和negb_involutive.如果我将Basics.v的内容复制到Induction.v中，它将进行编译，但是显然这不是可行的方法.

I'm using CoqIDE to complete the exercises in the Software Foundations book about Coq. I can successfully compile Basics.v, resulting in Basics.vo and Basics.glob in my directory. When I try to run Induction.v, it works. When I try to compile it, it complains about tons of missing references, such as evenb and negb_involutive. If I copy Basics.v contents into Induction.v it compiles, but obviously this is not the way to go.

这不是问题编译基础知识.检查Basics.vo是否在目录中.现在编译Induction.v.最后一步失败.

Compile Basics.v. Check if Basics.vo is in the directory. Now compile Induction.v. This last step fails.

推荐答案

我自己遇到了此错误.尝试从Software Foundations文件所在的目录打开CoqIDE，然后从那里编译.如果您使用的是Linux，只需打开一个终端，转到该目录，然后在其中键入coqide.我不知道如何在其他系统上执行此操作，例如Mac OS，但我确实注意到，仅通过图标打开应用程序会导致应用程序失败.

I have experienced this error myself. Try opening CoqIDE from the same directory where the Software Foundations files are, and compile from there. If you're on Linux, just open a terminal, go to that directory, and type coqide there. I don't quite know how to do this on other systems, e.g. Mac OS, but I did notice that just opening the app through the icon makes it fail.

这篇关于参考"X"指的是"X".在当前环境中找不到的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！