为什么我的类型记录排序显示为Set sort？

Question

当我使用Record宏创建记录类型时，它显示为Set排序而不是Type sort。

我创建了一个显示相同行为的最小测试示例：

Record little_test : Type :=
  {
    bit1 : nat;
    bit2 : nat;
  }.

Check little_test.

little_test
     : Set

Answer 1

Set只是Type无限等级中的最低级别。因为Coq的宇宙是累积的，这意味着little_test也存在于每一个更高的层次。通常，您不希望将类型限制在更高级别，因此Coq只是最小化Universe级别。如果你真的希望little_test处于更高的水平，你可以明确地要求它。

如果您使用的是CoqIDE，请在“视图”菜单中设置“显示Universe级别”而不是Set Printing Universes.。其他IDE（Proof General等）也可能有自己的方式来显示Universe级别。

Set Printing Universes.

Record little_test@{i} : Type@{i} :=
  {
    bit1 : nat;
    bit2 : nat;
  }.

Check little_test.

这种方法声明了一个固定的宇宙级别（little_set.i）并迫使little_set居住在Type@{little_test.i}。如果您已经拥有其他位置的Universe级别，则可以不使用Universe级别的声明。

Set Printing Universes.

Record little_test1@{i} : Type@{i} :=
  {
    bit1 : nat;
    bit2 : nat;
  }.

Record little_test2 : Type@{little_test1.i} :=
  {
    bit3 : nat;
    bit4 : nat;
  }.

Check little_test1.
Check little_test2.

在这种方法中，little_test1和little_test2具有相同的最低水平（但请记住，宇宙累积性意味着它们都栖息在每个更高的水平）。

这最后的方法宣称无限多的little_tests - 每个宇宙级别一个。

Set Printing Universes.
Unset Universe Minimization ToSet.

Polymorphic Record little_test@{i} : Type@{i} :=
  {
    bit1 : nat;
    bit2 : nat;
  }.

Check little_test.

但是，默认情况下，当您使用没有Universe参数的little_test时，Coq将最小化Universe级别（如果不存在约束，则为Set），因此我们必须使用Unset Universe Minimization ToSet来更改此行为。如果你想让你所有的Records和Inductive类型像这样多态，你可以Set Universe Polymorphism。请注意，您仍然必须使用@{i}（或Universe级别的其他名称）来指示多态性的位置。