Support for Sort*
and Type*
. #
These elaborate as Sort u
and Type u
with a fresh implicit universe variable u
.
The syntax variable (X Y ... Z : Sort*)
creates a new distinct implicit universe variable
for each variable in the sequence.
Equations
Instances For
The syntax variable (X Y ... Z : Type*)
creates a new distinct implicit universe variable
> 0
for each variable in the sequence.