Timeline for Coq error: The reference evenb was not found in the current environment
Current License: CC BY-SA 3.0
8 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jun 11, 2022 at 16:42 | comment | added | Charlie Parker |
I got Error: The reference lia was not found in the current environment. -- how does one fix that?
|
|
| Sep 12, 2018 at 13:54 | answer | added | Jisuk Byun | timeline score: 3 | |
| Jun 9, 2017 at 10:55 | answer | added | Daco Harkes | timeline score: 3 | |
| Nov 25, 2016 at 12:04 | comment | added | Mirzhan Irkegulov |
Try prepending Add LoadPath "." at the beginning of Induction.v as per this answer.
|
|
| Oct 5, 2016 at 11:39 | history | edited | Anton Trunov |
tag cleanup
|
|
| Apr 15, 2016 at 20:54 | answer | added | Ugur Koc | timeline score: 1 | |
| Apr 3, 2016 at 18:02 | comment | added | Arthur Azevedo De Amorim | 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? | |
| Apr 3, 2016 at 4:00 | history | asked | user2908789 | CC BY-SA 3.0 |