type of 'list'

Stream: Lean for teaching

[Daniel Ever]

I apologize if that was covered before, but I'm now reading through Theorem proving in Lean and stumbled upon the 'list' thing. Why does 'list' has a type of Type u → Type u? Shouldn't the type of lists of elements of some type have its own type? If not, why it's so? The same seems to apply to 'prod' and some others. Thanks in advance.

[Notification Bot]

This topic was moved by Anne Baanen to #new members > type of 'list'