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
Software Foundations: minustwo not found in Poly.v Using Rocq software-foundations	6	737	July 28, 2021
Issue with importing definitions from previous chapter in CoqIDE Using Rocq software-foundations	24	295	July 10, 2024
How to import a file in Coq? Using Rocq	6	4362	June 8, 2020
How to use "Require Import" Using Rocq	1	2199	December 6, 2019
Building a project with coq_makefile, using a library specified in .coqrc Using Rocq	0	699	January 25, 2022

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

Related topics