0

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

  1. 我尝试Require Import HoTT.在 CoqIde 中编写并得到错误Unable to locate library HoTT. (While searching for a .vos file.)
  2. 我试着写From HoTT Require Import Basics.或者Require Import HoTT.Basics.我得到了错误Notation "~ _" is already defined at level 75 with arguments constr at level 75
  3. 但是，我可以加载一些库，例如UnivalenceAxiom通过编写From HoTT Require Import UnivalenceAxiom. 所以我的问题是如何在我的 CoqIde 中导入 HoTT 库？
4

2 回答 2

1

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

-arg -noinit
-arg -indices-matter

在您的项目根文件夹中（您使用 HoTT 从该文件夹加载文件）。

如果您能告诉我们您在哪里寻找这方面的文档，这将有所帮助，以便我们对其进行调整。例如，它记录在 opam 中（如果你这样做的话opam show coq-hott），但我想这不是他最明显的地方。

于 2021-12-09T09:31:29.837 回答
0

在导入HoTT之前，我遇到了完全相同的问题并通过将此行添加到文件顶部来“修复”它：Reserved Notation "~ x" (at level 35, right associativity).

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

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

从那以后它工作得很好。令人困惑的是，Emacs 将符号行突出显示为错误，但它加载正常，我可以继续前进。IMO 这似乎是 Coq 最新版本的一个错误。

于 2021-12-20T23:59:50.897 回答