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.