布尔值的归纳定义

Question

平凡的，我试图将自己的bool类型定义为：

Inductive mybool : Type :=
    | true
    | false.

然后我做了一个“打印mybool”。但输出说

Inductive mybool : Set := true : mybool | false : mybool.

为什么“mybool”的类型是Set而不是Type？

Answer 1

Coq使用所谓的“宇宙最小化”将归纳类型放入尽可能小的宇宙中。由于mybool不依赖于任何其他类型且不进行任何通用量化，因此可以安全地放入Type的（第二）Set最低级别。最低级别是Prop，但归纳类型只放在Prop中，如果它们只有一个构造函数（对此有一些例外），或者它是明确注释的。

请注意，Coq的宇宙是累积的，所以mybool确实在Type的每个级别，但它只显示最小级别。