CoqIde中如何导入Coq库HoTT
How to Import Coq library HoTT in CoqIde
我想在我的 CoqIde 中使用 HoTT 库。我的环境是Coq_Platform_2021.09.0.8.13-installer-windows-x86_64-signed，试了很多方法。
- 我尝试在 CoqIde 中编写
Require Import HoTT. 并得到错误 Unable to locate library HoTT. (While searching for a .vos file.)
- 我尝试写入
From HoTT Require Import Basics. 或 Require Import HoTT.Basics.，但出现错误 Notation "~ _" is already defined at level 75 with arguments constr at level 75
- 但是，我可以通过写
From HoTT Require Import UnivalenceAxiom. 加载一些库，例如 UnivalenceAxiom
所以我的问题是如何在我的 CoqIde 中导入 HoTT 库？
您需要放置一个名为 _CoqProject 的文件，其内容如下：
-arg -noinit
-arg -indices-matter
在您的项目根文件夹中（使用 HoTT 从中加载文件）。
如果您能告诉我们您在哪里查找这方面的文档，我们会有所帮助，以便我们进行调整。它是例如在 opam 中有记录（如果你这样做 opam show coq-hott），但我想这不是最明显的地方。
我遇到了完全相同的问题，并在导入 HoTT 之前通过将此行添加到我的文件顶部来“修复”它：Reserved Notation "~ x" (at level 35, right associativity).
所以我的整个文件看起来像：
Reserved Notation "~ x" (at level 35, right associativity).
From HoTT Require Import HoTT.
从那以后一切正常。令人困惑的是，Emacs 将符号行突出显示为错误，但它加载正常，我可以继续前进。在我看来，这似乎是 Coq 最新版本的错误。
我想在我的 CoqIde 中使用 HoTT 库。我的环境是Coq_Platform_2021.09.0.8.13-installer-windows-x86_64-signed，试了很多方法。
- 我尝试在 CoqIde 中编写
Require Import HoTT.并得到错误Unable to locate library HoTT. (While searching for a .vos file.) - 我尝试写入
From HoTT Require Import Basics.或Require Import HoTT.Basics.，但出现错误Notation "~ _" is already defined at level 75 with arguments constr at level 75 - 但是，我可以通过写
From HoTT Require Import UnivalenceAxiom.加载一些库，例如UnivalenceAxiom所以我的问题是如何在我的 CoqIde 中导入 HoTT 库？
您需要放置一个名为 _CoqProject 的文件，其内容如下：
-arg -noinit
-arg -indices-matter
在您的项目根文件夹中（使用 HoTT 从中加载文件）。
如果您能告诉我们您在哪里查找这方面的文档，我们会有所帮助，以便我们进行调整。它是例如在 opam 中有记录（如果你这样做 opam show coq-hott），但我想这不是最明显的地方。
我遇到了完全相同的问题，并在导入 HoTT 之前通过将此行添加到我的文件顶部来“修复”它：Reserved Notation "~ x" (at level 35, right associativity).
所以我的整个文件看起来像：
Reserved Notation "~ x" (at level 35, right associativity).
From HoTT Require Import HoTT.
从那以后一切正常。令人困惑的是，Emacs 将符号行突出显示为错误，但它加载正常，我可以继续前进。在我看来，这似乎是 Coq 最新版本的错误。