Inductive type display is misleading

[eric-wieser]

The docs for list render as:

However, if we run that code:

inductive {u} my_list (T : Type u) : Type u
| nil : Π {T : Type u}, list T
| cons : Π {T : Type u}, T → list T → list T

we get the error

universe level of type_of(arg #2) of 'my_list.nil' is too big for the corresponding inductive datatype

This was reported on Zulip too. #151 made this a little better by at least making some arguments implicit.