ssrnat是否包含在Coq 8.7中？

Question

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

From Coq Require Import ssreflect ssrfun ssrbool.

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

Answer 1

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

在Coq 8.7中，仅包括战术语言本身ssreflect以及一些基本的支持库ssrfun ssrbool。

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

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