leanprover
Over saturated Lean constructor not documented
https://lean-lang.org/doc/reference/latest/The-Type-System/Inductive-Types/#inductive-type-universe-levels
^ here says:
Type constructors of inductive types must either inhabit a universe or a function type whose return type is a universe. Each constructor must inhabit a function type that returns a saturated application of the inductive type. If the inductive type's universe is Prop, then there are no further restrictions on universes, because Prop is impredicative. If the universe is not Prop, then the following must hold for each parameter to the constructor:
If the constructor's parameter is a parameter (in the sense of parameters vs indices) of the inductive type, then this parameter's type may be no larger than the type constructor's universe.
All other constructor parameters must be smaller than the type constructor's universe.
inductive Vec (α : Type u) : Nat → Type u
| zero : Vec α 0
| «++» : Vec α n → α → Vec α n.succ
Vec α is "saturated". Vec α 0 is "over saturated". Just from reading the the text section above doesn't tell you this.
Type constructors of inductive types must either inhabit a universe or a function type whose return type is a universe.
The return type is Nat → Type u, not a universe.
