Hi! What I did when I had this problem is made sure I downloaded the entire LF repository (So one giant folder that has everything in it) which you can just download from the Foundations Textbook Github. That already has the make file and everything like that inside of it. So after downloading it, I just opened up Basics in Coq, when to the “Compile” header next to tools at the very top, did compile buffer. It should make the files that you need to import it from then on.
1 Like