coq - 什么是 GroupScope？

Question

在 ssreflect 的所有 coq 代码中都有这个语句

Import GroupScope.

是什么GroupScope？如果它是另一个文件，我可以从哪里下载它？

Answer 1

GroupScope是在MathComp库（以前是 SSR 的一部分）的fingroup模块中 定义的模块。定义如下：

Module GroupScope.
Open Scope group_scope.
End GroupScope.

因此，导入GroupScope的效果是使group_scope当前文件中的所有符号都可用，但有一点不同，如源代码中所述：

可以导入此模块以在本地打开文件的组元素操作范围，而无需将 Open 导出到该文件的客户端（就像 Open 一样）。