coq - ssrnat 是否包含在 Coq 8.7 中？

Question

Coq 8.7 集成了流行的 Ssreflect 库。因此可以通过以下方式导入其库：

From Coq Require Import ssreflect ssrfun ssrbool.

但是，当我尝试导入ssrnat它时，它会抱怨它是Unable to locate library ssrnat with prefix Coqssrnat，而且我也无法在磁盘上的 Coq 发行版中找到 ssrnat。出于ssrnat某种原因故意不包含，或者文件夹到另一个模块中，或者我的安装有问题？

Answer 1

ssrnat不包含在主要的 Coq 发行版中，尽管有一天我们希望提供一个扩展的发行版，默认情况下可以使用更多的库。

在 Coq 8.7 中，只包含了策略语言本身ssreflect以及一些基本的支持库ssrfun ssrbool。

我们没有包含更多内容的原因是因为ssrnat使用了 math-comp 数学层次结构，所以这是一个更具“侵入性”的更改。

幸运的是，由于包含了插件，安装 ssrnat 是一项非常容易的任务。