时间戳

首页 > 解决方案 > 要求每个文件中的导出更改要求

module - 要求每个文件中的导出更改要求

问题描述

我是 Coq 的新手，目前正在阅读 Software Foundations 系列教程。

然而，我一直发现自己Require Export在第一次尝试时很难让零件工作，每个文件似乎都需要一个新的策略才能工作。然而，这一次，我完全被困住了。

在一个文件（Lists.v）中，我可以简单地编写 From LF Require Export Induction.，并且让它工作得很好。

在下一个（Poly.v）中，我根本无法加载 Lists 模块，

From LF Require Export Lists. 
(* ==> Cannot find a physical path bound to logical path matching suffix
<> and prefix LF. *)

除非我先将加载路径添加到当前文件夹：

Add LoadPath "~/Documents/code/coq/".
From LF Require Export Lists. (* Works perfectly! *)

但是，在下一章中，似乎没有任何效果。

这是我尝试过的：

From LF Require Export Poly.
(* ==> Cannot find a physical path bound to logical path matching suffix
<> and prefix LF. *)

Add LoadPath "~/Documents/code/coq/".
From LF Require Export Poly.
(* ==> The file /Users/coffee/Documents/code/coq/LF/Poly.vo contains library Poly
and not library LF.Poly *)

Add LoadPath "~/Documents/code/coq/LF/".
From LF Require Export Poly.
(* ==> Cannot find a physical path bound to logical path matching suffix
<> and prefix LF. *)

Add LoadPath "~/Documents/code/coq/LF/".
Require Export Poly.
(* ==> Cannot load LF.Basics: no physical path bound to LF *)

可以肯定地说：我在这里不知所措，我不知道我在做什么或为什么它不起作用。它以前有效，我在网上找不到任何东西似乎可以给出任何好的答案。

我的 _CoqProject 文件包含-Q . LF

我在 Windows 和 Mac 上都遇到了这个问题。

我正在使用最新版本的 CoqIDE。

标签： modulecoqcoqidelogical-foundations

解决方案

推荐阅读