我正在尝试通过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）时，我收到错误消息“错误：在当前环境中找不到引用偶数。” - 即使在编译Basics.v之后。有什么想法吗？
我可以确认从同一目录打开CoqIDE可以在macOS上运行：
cd <sf-dir>; /Applications/CoqIDE_8.5.app/Contents/MacOS/coqide
来自：The reference "X" was not found in the current environment
尝试擦除与Coq或软件基础书相关的地址中的每个空白字符。
在我的情况下，当我努力与文件
C：\ Users \ XxX \ Documents \ software foundation \ lf \ Induction.v
，CoqIDE未能执行From LF Require Export Basics并定义evenb_S定理。另外，当在CoqIDE中使用[Compile] - [Compile buffer]功能进行Basics.vo时，我看不到像Basics.glob或Basics.v这样的文件。
当我将文件夹名称更改为时，一切正常
C：\ Users \ XxX \ Documents \ software foundation \ of \ Basic.v
Coq安装人员已经通知了这个>> Link to the screenshot image of Coq setup
使用Basic.v命令编译coqc Basics.v应该在同一目录中生成Basic.vo和Basic.glob文件。那么你也可以在同一个目录中编译Induction.v; coqc Induction.v。