我正在使用CoqIDE完成关于Coq的软件基础书中的练习.我可以成功编译Basics.v,在我的目录中生成Basics.vo和Basics.glob.当我尝试运行Induction.v时,它可以工作.当我尝试编译它时,它会抱怨大量缺少的引用,例如evenb和negb_involutive.如果我将Basics.v内容复制到Induction.v中,它会编译,但显然这不是要走的路.
这不是问题的重复Coq错误:在当前环境中找不到引用evenb,因为我已经完成了这些事情:
编译Basics.v.检查Basics.vo是否在目录中.现在编译Induction.v.最后一步失败了.
我自己也经历过这个错误.尝试从Software Foundations文件所在的同一目录中打开CoqIDE,然后从那里进行编译.如果你在Linux上,只需打开一个终端,转到该目录,然后coqide在那里输入.我不太清楚如何在其他系统上执行此操作,例如Mac OS,但我注意到只需通过图标打开应用程序就会失败.
| 归档时间： |
|
| 查看次数： |
1511 次 |
| 最近记录： |