如何在HoTT中导入Coq库CoqIde

Question

我想在我的HoTT中使用CoqIde库。我的环境是Coq_Platform_2021.09.0.8.13-installer-windows-x86_64-signed，我尝试过很多方法。

我试着用Unable to locate library HoTT. (While searching for a .vos file.)

• I编写Require Import HoTT.和错误，Notation "~ _" is already defined at level 75 with arguments constr at level 75

• However，试图编写From HoTT Require Import Basics.或Require Import HoTT.Basics.，我可以通过编写From HoTT Require Import UnivalenceAxiom.加载一些库，比如UnivalenceAxiom，所以我的问题是如何在CoqIde?

中导入HoTT库

Answer 1

您需要放置一个名为_CoqProject的文件，其内容如下：

-arg -noinit
-arg -indices-matter

在您的项目根文件夹中(您使用HoTT从其中加载文件)。

如果您能告诉我们您在哪里查找有关这方面的文档，这样我们就可以对其进行调整，这将有帮助。例如，它被记录在opam (比如说，如果你做了opam show coq-hott)，但我想这不是最明显的地方寻找他的。

Answer 2

在导入HoTT：Reserved Notation "~ x" (at level 35, right associativity).之前，我将这一行添加到文件的顶部，从而解决了同样的问题。

所以我的整个文件看起来是：

Reserved Notation "~ x" (at level 35, right associativity).
From HoTT Require Import HoTT.

从那以后一切都很顺利。令人困惑的是，Emacs将符号行突出显示为一个错误，但它加载得很好，我可以继续。国际海事组织，这似乎是一个新版本的Coq的错误。