Индуктивное определение логического

Question

Обычно я пытаюсь определить свой собственный тип bool следующим образом:

Inductive mybool : Type :=
    | true
    | false.

Затем я делаю «Print mybool».но вывод говорит:

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

Почему тип "mybool" установлен, но не тип?

Answer 1

Coq использует так называемую «минимизацию вселенной», чтобы поместить индуктивные типы в наименьшую возможную вселенную.Поскольку mybool не зависит от каких-либо других типов и не выполняет какого-либо универсального количественного определения, его можно смело ставить на (второй) самый низкий уровень Type, который равен Set.Самый низкий уровень - Prop, но индуктивные типы помещаются в Prop, только если у них есть только один конструктор (есть некоторые исключения из этого), или если он явно аннотирован.

Обратите внимание, что юниверсы Coqкумулятивный, поэтому mybool действительно на каждом уровне Type, но показывает только минимальный уровень.