Coq错误：在当前环境中找不到参考evenb [英] Coq error: The reference evenb was not found in the current environment

问题描述

我正在尝试阅读《 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 ），我得到了错误消息错误：在当前环境中找不到参考evenb。 -即使在编译Basics.v。之后知道为什么吗？

I'm trying to go through the Software Foundations Coq book (http://www.cis.upenn.edu/~bcpierce/sf/current/toc.html), but when I compile Induction.v (which looks like http://www.cs.uml.edu/~rhenniga/coq/sf_induction.html), I get the error message "Error: The reference evenb was not found in the current environment." -- even after compilation of Basics.v. Any ideas why?

推荐答案

尝试擦除与Coq或软件基础书相关的地址中的每个空白字符。

Try to erase every blank character in the address related to Coq or software-foundation book.

对于我来说，当我在处理文件时遇到困难

In my case, when I struggled with the file

C：\Users\XxX\Documents\软件基金会\lf\Induction.v

C:\Users\XxX\Documents\software foundation\lf\Induction.v

，CoqIDE无法执行LF Require Export Basics 中的和定义 evenb_S 定理。另外，我看不到 Basics.vo 或 Basics.glob > Basics.v 在CoqIDE中具有[编译]-[编译缓冲区]功能。

, CoqIDE failed to execute From LF Require Export Basics and to define evenb_S theorem. Also, I couldn't see any files like Basics.vo or Basics.glob created when Basics.v with [Compile] - [Compile buffer] function in CoqIDE.

当我将文件夹名称更改为

Everything works fine when I change my folder name to

C：\Users\XxX\Documents \softwarefoundation\lf\Basic.v

C:\Users\XxX\Documents\softwarefoundation\lf\Basic.v

Coq安装程序已经通知了此>>
链接到Coq的屏幕快照设置

The Coq installer had already informed this >> Link to the screenshot image of Coq setup

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