Coq error: parity not found in current environment

Question

I try to go through the book Software Foundations Coq ( 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 ), the error message "Error: No reference parity was found in the current environment" appears. - even after compiling Basics.v. Any ideas why?

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 cd <sf-dir>; /Applications/CoqIDE_8.5.app/Contents/MacOS/coqide

from: Link "X" not found in current environment

Answer 2

Compiling Basic.v with the coqc Basics.v should contain the Basic.vo and Basic.glob in the same directory. Then it will be good for you to compile Induction.v in the same directory; coqc Induction.v .