如何編譯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

提供有關編譯的詳細信息（如你是否使用命令行或代碼編輯器，勒柯克版本，教材版本等）可能對解決您的問題很有用。