I am currently going through the exercises in the file Poly.v from the book Logical Foundations. When trying to step forward to the line Example test_doit3times: doit3times minustwo 9 = 3. I get the error The reference minustwo was not found in the current environment.
I tried running make Basics.vo Induction.vo Lists.vo but that didn’t help.
I suppose I must have missed a step somewhere but I’m not sure which one it is. Any idea? Thanks in advance.
The book seems to assume that library exports are transitive, which is not true. So, you should change the line
From LF Require Export Lists.
into
From LF Require Export Basics Lists.
This file compiles just fine for me under 8.13 – what version of Coq are you using, @YaVeremos?
I am using version 8.13.2. By the way, I am really enjoying learning through your books. They are challenging and fun. I am so grateful that you made them publicly available.
Thank you Silene, your suggested change solved the problem.
@bcpierce For what it’s worth the cause of the error turned out to be very simple. I am using VSCode along with its Coq extension and I didn’t notice that I opened the project’s parent directory rather than the project’s directory itself. I suppose the Coq extension must look up in the opened directory for files to import and can’t find anything there.
Many thanks for the update – I’ll try to find a place to document this gotcha.