Этот ответ состоит из двух частей.
Что означает Definition x := y : A?
Это означает, что x определено как y, и есть утверждение, что y имеет тип A. Обычно это утверждение излишне, потому что Coq может определить тип y сам по себе. Однако иногда термин имеет слишком много неявных частей, поэтому утверждение необходимо для определения всех этих неявных частей.
Что означает Type : Type? 1014 *
Примером наличия неявных частей является Type. Вас может удивить, что в Coq нет ни одного Type. Вместо этого существует бесконечная иерархия типов Type@{0}, Type@{1}, Type@{2}… с Type@{i} : Type@{j}, если i < j. Это означает, что каждая вселенная (Type@{j}) содержит в качестве элемента каждую вселенную с меньшим уровнем.
Однако по умолчанию Coq явно не показывает эти "уровни вселенной". Coq, как правило, достаточно умен, чтобы понять уровни вселенной (или сделать их общими), не беспокоя вас. Вы можете указать Coq показывать их с помощью обычной команды Set Printing Universes. или установив параметр в меню IDE, если вы его используете. Затем, после определения x, как вы сделали, с помощью команды Print x. отобразится
x =
Type@{Top.2}
: Type@{Top.1}
(* {Top.2 Top.1} |= Top.2 < Top.1
*)
Итак, x определено как Type@{Top.2} и имеет тип Type@{Top.1}. Top.1 и Top.2 являются просто именами для общих уровней вселенной. Часть сообщения внизу просто утверждает, что Top.2 должно быть меньше Top.1. Это потому, что нам нужно Type@{Top.2}, чтобы иметь тип Type@{Top.1}. Помните, что вселенные содержат вселенные под ними, но не те, что над ними.
Дополнительный вопрос: почему существует несколько уровней Type?
Короче говоря, если бы у нас был только один Type с Type : Type, можно было бы показать, что система несовместима. Это называется парадоксом Жирара (или более простым вариантом, известным как парадокс Хюркенса). См. этот ответ для некоторых хороших деталей.
Если вам нужно другое объяснение вселенных Кока, см. этот замечательный ответ .