How can we import beq_nat from Basics.v - Similar to 43

[woong8556]

I have the same problem with the issue #43 . The same error occurs when I compile the code Check beq_nat. The error message is: Warning: query commands should not be inserted in scripts Error: The reference beq_nat was not found in the current environment.

I'm working in Windows 7, so some kinda things like make don't seem to be the solution. To cope with it, I think of not using beq_nat at all. Instead, I will use my own Fixpoint beq_nat_mimic, which I will define by myself so that it works just same as ordinary beq_nat. Is that OK?

[jeehoonkang]

• It's time to submit, so for now, please do as you say.
• However, make IS THE SOLUTION. From now on, install make in Windows, or use martini@snucse.org instead.

Jeehoon

[jaewooklee93]

I guess that Windows version of CoqIde is also able to make object files, *.vo.

How about trying this?

1. Make certain that your Assignment03.v and Basics.v files are in the same folder.
2. Open Assignment03.v with CoqIde.
3. From the menu bar, Compile>Make makefile
4. Compile>Make
5. Now you have Basics.vo in your working directory.

Then you are probably able to execute Require Import Basics. and Check beq_nat..

[woong8556]

Wow, it really was solved! I mis-thought that make would be a Linux command or something. Thank you jeehoonkang and jaewooklee93, for being specific about solving this.