为什么我的类型排序记录显示为集合排序?

Set 只是无限层次中的最低层次 Type . 因为Coq的宇宙是累积的,这意味着 little_test 也居住在更高的层次。一般来说,你不想把你的类型限制在更高的层次上,所以Coq只是最小化了宇宙层次。如果你真的想 小考

如果使用CoqIDE,请在“视图”菜单中设置“显示宇宙级别”,而不是 Set Printing Universes. . 其他ide(Proof-General等)也可能有自己的方式来显示宇宙级别。

Set Printing Universes.

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

Check little_test.

这种方法声明了一个固定的宇宙级别( little_set.i Type@{little_test.i} . 如果你已经从其他地方得到了一个宇宙级别,那么你可以停止声明宇宙级别。

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

最后一种方法声明无限多 小考 每个宇宙级别一个。

Set Printing Universes.
Unset Universe Minimization ToSet.

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

Check little_test.

小考 没有宇宙参数 套 Unset Universe Minimization ToSet 改变这种行为。如果你想要你所有的 Record s和 Inductive 类型是多态的,您可以 Set Universe Polymorphism . 注意你仍然需要使用 @{i} (或宇宙级别的其他名称)指示多态性的位置。