Zulip Chat Archive

Stream: Lean for teaching

Topic: type of 'list'

Daniel Ever (Feb 01 2022 at 17:13):

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 (Feb 01 2022 at 17:17):

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

Last updated: Dec 20 2023 at 11:08 UTC