At this point in the text, reading linearly, universes have not yet been introduced and I could not figure out what this syntax meant (the : Type) and what its purpose is.
inductive Option (α : Type) : Type where
| none : Option α
| some (val : α) : Option α
I briefly thought a was a lean3 vs lean4 thing because of the difference here:
Option
At this point in the text, reading linearly, universes have not yet been introduced and I could not figure out what this syntax meant (the
: Type
) and what its purpose is.I briefly thought a was a lean3 vs lean4 thing because of the difference here:
: Type
): Type
)I wondered if it could be left out, but the 'Messages You May Meet' example no longer produces a message if I remove
: Type
.I understand it has something today with the different levels of types ( https://lakesare.brick.do/on-universes-in-lean-vByqZWpNnrEJ )
Not sure if there is a way to uncover this linearly better?