在 coqtop 中启用显式类型索引？

Question

在 Coq 中有一个类型层次结构，每个类型表示前一个类型，即 Type_0 : Type_1、Type_1 : Type_2 等等。然而，在 coqtop 中，当我键入 Check Type. 时，我得到 Type : Type ，这看起来像是一个矛盾，但并不矛盾，因为 Type 是隐式索引的。

问题：如何启用类型域的显式索引？

Answer 1

上面提到的@ejgallego 的简短回答是启用宇宙级别的打印：

Coq < Set Printing Universes.
Coq < Check Type.
Type@{Top.1}
     : Type@{Top.1+1}
(* Top.1 |=  *)

概念上确实存在一个类型层次结构，可以称为 Type@{1}、Type@{2} 等。但是，Coq 实际上维护了全域索引的符号和它们之间的关系（全域约束），而不是明确的数字。约束保持一致，因此始终可以以一致的方式为每个符号分配一些明确的数字。

在上面的输出中，您可以看到 Coq 在 Check Type. 命令中为 Type 创建了一个宇宙级别 Top.1。它的类型总是高一级，Coq 没有用表达式 Top.1+1 的另一个符号来做到这一点。使用 Set Printing Universes 约束列表也作为注释输出；在这种情况下，它在上下文 Top.1 中给出了一个符号，并且在右侧没有约束。

Coq 维护着它迄今为止创建的宇宙级别和约束的全局列表。您可以阅读 CPDT 中对宇宙级别和约束的更详尽解释：http://adam.chlipala.net/cpdt/html/Universes.html.

在 coqtop 中启用显式类型索引？

Enable explicit Type indices in coqtop?

coq