https://coq.vercel.app/ext/sf/lf/full/Induction.html I am using VSCode Coq extension. I am having an error with From LF Require Export Basics. in Induction.v [image] I ran coq_makefile -f _CoqProject *.v -o Makefile and make but I get an error Cannot find a physical path bound to logical pa…

I think the problem is with the "coqtop.coqProjectRoot" setting - according to the documentation , it is relative to the workspace root, which I think is the dev-notes directory (the top-level you have open in VSCode), so try setting it to "coq" (the directory that contains the .v and _CoqProject fil…

How to import Basics.v in Induction.v of LF using VS Coq extension

Using Rocq

brando90 February 24, 2023, 11:49pm 8

Topic		Replies	Views
Issue with importing definitions from previous chapter in CoqIDE Using Rocq software-foundations	24	522	July 10, 2024
How to have vscode find coq? Using Rocq	5	4909	February 24, 2023
Software Foundations: minustwo not found in Poly.v Using Rocq software-foundations	6	761	July 28, 2021
Coqtop is not running Using Rocq	8	1002	September 8, 2023
How to import a file in Coq? Using Rocq	6	4618	June 8, 2020

How to import Basics.v in Induction.v of LF using VS Coq extension

Related topics