Hey all, weird question, probably simple answer.
I was trying to define some things and ran them all with scratch in the CoqIDE, and they work out fine. On the other hand, as soon as I put them into a named file, they do not work any more. I have included a simple example of this. I am not sure what's going on, I am just copying one page to another. working.PNG
Ah, are you using HoTT libraries? So the second file fails because it's being compiled with the stdlib disabled?
looks like the scratch file is not picking up the settings
I assume you have special options for hott somewhere, like _coqproject, but where is that?
Ha! Got me. That was it exactly. Thanks so much, I would have been at that forever.
Brandon Sisler has marked this topic as resolved.
I'm happy this helped!
And thanks for letting me know :-)
Last updated: Dec 05 2023 at 04:01 UTC