有人可以给我更多关于 Coq 中的一流模块的信息吗？我知道 Coq 中的模块不是一流的。我想知道原因是什么？将来 Coq 中的模块有可能是一流的吗？
非常感谢
最佳答案
我不确定，但据我了解，它主要来自两点:
Coq 是保守的。因为它的一些主要应用是在验证中，所以 Coq 大多将自己限制在语义易于理解的构造上。
在依赖类型设置中，一流模块相当微妙且无法完全理解。特别是，您希望定义的多少计算/归约行为在外部可见一个模块？如果根本没有，那么这已经作为记录类型可用。但是，如果部分或全部减少行为是可见的，那么就很难准确量化到底有多少，因此很难分析结果模块的语义。
我不是相关文献的专家，所以我对2的看法很可能是错误的，但我的印象是这是基本情况。
关于coq - Coq 中的一流模块，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/15940367/