如何编译lists.v在COQ？

Question

我使用的辅助证明COQ，我的第一个问题是关于Induction.v文件，为什么我们使用Require Export Basics，而不是Require Import basics？此外，当我们做Export basics.v，即使我改变了基本的名称Mybasics.v为什么工作？

是什么Require Export Basics.办？它是导入还是导出？

我试图编译induction.v后执行lists.v，但它不能正常工作，它说

无法找到库感应。

我该如何解决这个问题？

Answer 1

你工作的软件基础？您需要将该文件夹添加到COQPATH。因为一般的证据已办理的是，我敢打赌，你正在使用coqide，不是吗？

您的问题的其余部分都可以通过查阅coq ref手册：https://coq.inria.fr/refman/toc.html来解决。

Answer 2

Require Import和Require Export之间的差异可以在这里找到：https://coq.inria.fr/refman/vernacular.html#hevea_command115

提供有关编译的详细信息（如你是否使用命令行或代码编辑器，勒柯克版本，教材版本等）可能对解决您的问题很有用。