Coq error: The reference evenb was not found in the current environment

Question

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?

We need some more context to know what could be wrong. Are you using CoqIDE? Is Basics.v on the same directory as Induction.v? Is the compiled file Basics.vo actually showing up on that directory? — Arthur Azevedo De Amorim, Apr 03 '16 at 18:02
Try prepending `Add LoadPath "."` at the beginning of `Induction.v` as per [this answer](http://stackoverflow.com/a/16203673/596361). — Mirzhan Irkegulov, Nov 25 '16 at 12:04
I got `Error: The reference lia was not found in the current environment.` -- how does one fix that? — Charlie Parker, Jun 11 '22 at 16:42

score 3 · Answer 1 · answered Jun 09 '17 at 10:55

3

I can confirm that opening CoqIDE from the same directory works on macOS: cd <sf-dir>; /Applications/CoqIDE_8.5.app/Contents/MacOS/coqide

from: The reference "X" was not found in the current environment

answered Jun 09 '17 at 10:55

Daco Harkes

296
3
13

I got `Error: The reference lia was not found in the current environment.` -- how does one fix that? – Charlie Parker Jun 11 '22 at 16:42

score 3 · Answer 2 · answered Sep 12 '18 at 13:54

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\software foundation\lf\Induction.v

, 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

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

I got `Error: The reference lia was not found in the current environment.` -- how does one fix that? — Charlie Parker, Jun 11 '22 at 16:42

score 1 · Answer 3 · answered Apr 15 '16 at 20:54

1

Compiling Basic.v with coqc Basics.v command should produce Basic.vo and Basic.glob files in the same directory. Then you should be fine with compiling Induction.v in the same directory as well; coqc Induction.v.

answered Apr 15 '16 at 20:54

Ugur Koc

53
7

Coq error: The reference evenb was not found in the current environment

3 Answers3

Linked