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?

Eusebioeusebius

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? – Himation

Try prepending Add LoadPath "." at the beginning of Induction.v as per this answer. – Wigging

I got Error: The reference lia was not found in the current environment. -- how does one fix that? – Andantino

Answer 1

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

Chloric

I got Error: The reference lia was not found in the current environment. -- how does one fix that? – Andantino

Answer 2

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

Found

I got Error: The reference lia was not found in the current environment. -- how does one fix that? – Andantino

Answer 3

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.

Spirituous