在Coq中导入Hott库
我正在尝试在COQ中使用COQ-HOTT库，但是导入无法正常工作。我正在coqorg/coq的容器中工作：最新 docker image。启动容器后，我完成了以下操作：
OPAM在容器终端中安装COQ-HOTT。- 将
vscode连接到容器中，并在此处安装了VSCOQ扩展名。 - 将路径设置为
_COQPROJECT和coqtop。 - 使用以下行创建
_COQPROJECT文件：
-arg -noinit
-arg -indices-matter
- 检查hott库位置：
/home/coq/.opam/4.05.0/lib/coq/coq/user-contrib/hott/hott
创建*。V文件以测试库后，我遇到了以下问题：
需要导入hott。给出
Cannot find a physical path bound to logical path HoTT.
- hott hott off inf infimend Import Import Basics。工作。工作，但是做
检查（2+2）。之后，
The term "2" has type "trunc_index" while it is expected to have type "Type".
- 从HOTT提供
需要导入代数。有效，但from hiott of hott ofimportion ofimportion分析。给予
Cannot find a physical path bound to logical path Analysis with prefix HoTT.
i根本不了解这种行为。它类似于这个问题，但仍然不同。我做错了吗？
根据OPAM COQ和coq-hott是8.15.1 [4.07.1+flambda 4.05.0]和分别分别为8.15 [4.05.0]。
I'm trying to use coq-hott library in Coq, but the import won't work. I'm working in the container of the coqorg/coq:latest docker image. After starting the container I've done the following:
opam install coq-hottin the container's terminal.- Hooked up
vscodeto the container and installed the VsCoq extension there. - Set the paths to
_CoqProjectandcoqtop. - Created the
_CoqProjectfile with the following lines:
-arg -noinit
-arg -indices-matter
- Checked the HoTT library location:
/home/coq/.opam/4.05.0/lib/coq/user-contrib/HoTT
After creating the *.v file to test the library I got the following problems:
Require Import HoTT.gives
Cannot find a physical path bound to logical path HoTT.
From HoTT Require Import Basics.works, but doingCheck (2+2).after that gives
The term "2" has type "trunc_index" while it is expected to have type "Type".
From HoTT Require Import Algebra.works butFrom HoTT Require Import Analysis.gives
Cannot find a physical path bound to logical path Analysis with prefix HoTT.
I don't understand this behavior at all. It is similar to this question, but still different. Am I doing something wrong ?
According to opam the packages versions for coq and coq-hott are 8.15.1 [4.07.1+flambda 4.05.0] and 8.15 [4.05.0] respectively.
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论