In §1.3.2.1 (“Messages You May Meet”)

Please quote the text that is incorrect:

In §1.3.2.1 (“Messages You May Meet”), the example

def thirtyEight : NaturalNumber := (38 : Nat)

is stated to be type-correct because “NaturalNumber is the same type as Nat—by definition.”

However, at this point in the text, NaturalNumber has not yet been introduced as a reducible alias (e.g. via abbrev NaturalNumber := Nat). When following the lesson line-by-line, Lean reports a type mismatch, since Nat does not coerce to an unrelated NaturalNumber.

The example works once NaturalNumber is defined using abbrev, which is explained later in the same section. It may help beginners (like me!) if the text either:

explicitly defines NaturalNumber as an abbrev before this example, or

clarifies that the example assumes NaturalNumber is a reducible alias of Nat.

Lean’s behavior here is correct; this appears to be a minor ordering/clarification issue in the lesson.

I thought I just share the feedback because I'm trying to learn LEAN, and I actually tried the example but got the mismatch type error, which struck me as odd. Either way, fun stuff! Thanks.

Start with §1.3.2.1, “Messages You May Meet,” and follow the lesson line by line around the NaturalNumber example and its later definition. Confirm the ordering or assumption that causes the mismatch, then update the explanation so the example is valid at that point; verify the lesson reads consistently from start to finish.