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 Coq

brando90 February 24, 2023, 11:49pm 8

Topic		Replies	Views
How to import a file in Coq? Using Coq	6	3580	June 8, 2020
How to use "Require Import" Using Coq	1	1981	December 6, 2019
Building a project with coq_makefile, using a library specified in .coqrc Using Coq	0	534	January 25, 2022
How does one import native cyclic integers in coq? Using Coq	3	223	August 2, 2023
Add LoadPath in Coq 8.12.2 Using Coq	5	2025	March 22, 2021

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

Related Topics