Incorrect number of universe levels parameters

Stream: lean4

[Uranus Testing]

This code works fine:

universe u

inductive E : Type u

But this throws an error “(kernel) incorrect number of universe levels parameters for 'T', #1 expected, #0 provided”:

inductive T : Type u
| intro

Is this OK?

[Leonardo de Moura]

Thanks for reporting this issue. I pushed a fix for it:
https://github.com/leanprover/lean4/commit/fb45eb49643b2abbc0d057d1fafc5e1eb419fc2a