Section 1.6: Polymorphism - `: Type`

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.

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:

• https://leanprover.github.io/theorem_proving_in_lean4/inductive_types.html (does not have : Type)
• https://leanprover.github.io/theorem_proving_in_lean/inductive_types.html (has : 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?

Start with Section 1.6 and compare the two linked inductive-types pages plus the linked universe explanation. Clarify why : Type appears at this point and how it relates to the later material, while keeping the “Messages You May Meet” example accurate after the explanation is added.