Explicit universes

Universes can now be instantiated explicitly. The syntax for a universe instantiation is

f u#universe_level_expression or f 'u_universe_level_variable

A universe level expression is either :

• a natural number n,
• a universe level variable 'ua,
• a sum u1 + u2 where at most one of the two universe expression contains a variable,
• or the maximum of a list of universe expressions max u1 u2 .. un.

A universe variable must be prefixed by 'u. Universe variables are bound at the enclosing toplevel definition in the syntactical order they were found in the term. If a term contains a universe level variable, there must not be any implicitly generalized universe variable, that is let f (a : Type 'ua) (b : Type) = 5 is invalid since there is an implicit unconstrained universe variable in (b:Type) whereas let g (a : Type 'ua) (b : Type) = a == b is valid.

For such an invalid term an error 'Generalized universe in a term containing explicit universe annotation' is reported. The compiler options --print_universes --print_bound_var_types may help debugging such an issue.

Note that 'u... is solely for universe variables, and you can't have type variables named 'u....