Include explicit Type indexes in coqtop?
There is a type hierarchy in Coq, each of which denotes the type of the previous ie Type_0: Type_1, Type_1: Type_2, etc. In coqtop
yet when I type Check Type.
, I get Type : Type
that looks like a contradiction, but not so much as Type
implicitly indexed.
Q: How do I enable explicit indexing of Type universes?
source to share
The short answer, mentioned above as @ejgallego, is to enable printing of universe levels:
Coq < Set Printing Universes.
Coq < Check Type.
Type@{Top.1}
: Type@{Top.1+1}
(* Top.1 |= *)
Conceptually, there is a hierarchy of types that can be named Type@{1}
, Type@{2}
etc. However, Coq actually supports characters for universe indexes and the relationships between them (universe constraints), not explicit numbers. The constraints are kept consistent so that it is always possible to sequentially assign some explicit number to each character.
In the above, you can see that Coq has created a universe level Top.1
for Type
within the command Check Type.
. Its type is always one level higher, which Coq does without another expression symbol Top.1+1
. The Set Printing Universes
list of restrictions is also displayed as a comment; in this case it gives one character in context Top.1
and no restrictions on the right side.
Coq maintains a global list of universe levels and the constraints it has created so far. You can read a more detailed explanation of universe levels and constraints in CPDT: http://adam.chlipala.net/cpdt/html/Universes.html .
source to share