docs: teach what 0.4.0 and 0.5.0 added, and correct what drifted

[simontreanor]

The course was written against a smaller language and a smaller library. Parts of it now describe a compiler that no longer behaves that way, and parts leave a learner unprepared for an error the compiler will actually raise. Everything below was checked by running it against the 0.5.0 binary.

Wrong

Lesson	What it claimed	What happens
8	let Some x = Some 1 reports "a let binding must always match"	It type-checks. parse_binding_target only enters the pattern grammar after ( or Ident {, so this parses as a function named Some with parameter x. The demo needs let (Some x) = …, which does produce the quoted error
17	"A recursive Pyfun function ... shares Python's call stack and its recursion limit"	A saturated self tail call has lowered to while True since #39. countDown 100000 0 runs fine
9, 6, 7, 21, 17	five quoted typed-hole notes	the stdlib sweep changed what fills the 6-fit cap
18	"The third built-in builder is async { }"	it is the fourth
6	quoted emitted Python for a record update	omits the _pf_t0 temporary that is actually emitted
5	defines let sign n	shadows the prelude's sign, so hovering it in an editor shows the built-in's docs

Lesson 9's stale note was the worst of them, because it broke the lesson's own point. It teaches "the compiler names your answer" directly above a note where String.upper no longer appears: the sweep added enough string -> string members that the intended answer is pushed past HOLE_FIT_CAP = 6 by the alphabetical tiebreak. The exercise now normalizes case with String.lower, which the note does name, and the lesson says plainly that try: is a shortlist rather than the full set.

Missing

Ordered by how soon a learner trips over it:

• extern import was taught nowhere. Since externs: refuse to guess an undecidable module prefix #50, a target like sys.stdout.flush is a hard compile error whose message asks for exactly that line. A learner following lesson 12's rule (extern name: Type = dotted.target) hits an error the course never mentions. Lesson 12 now walks the error and the fix.
• Instance-access externs (= .with_name) were referenced by lesson 23 as something "from lesson 12". Lesson 12 did not cover them. Now it does, and the cross-reference is true.
• Lesson 15 showed only values crossing a module boundary. Types cross too, and since the dogfooding fix a record may name another module's type, which is the change that lets a program split along its data instead of collapsing into one file.
• Seq was used in lesson 13 before being introduced anywhere, and laziness was the one collection idea the course did not teach. Lesson 7 now introduces it, with the two conventions the sweep settled: total functions that clamp, and Option from any accessor that can come up empty.
• Format was invisible outside quoted hole notes, where a learner met Format.padLeft as a suggestion for a module the course never named. input was untaught, so "how do I read from the user" had no answer on the site.
• The educator index listed five Going further lessons out of seven.

One compiler fix

Writing the Format section turned up that Format.thousands and Format.grouped carry each other's hover documentation. thousands : int -> float<'u> -> string formats a float with grouping and grouped : int<'u> -> string formats an integer, and MEMBER_DOCS had those two descriptions swapped. The padding pair's docs also omitted their fill argument, which their signatures take. This is what LSP hover and the hole notes serve, so it is documentation that happens to live in src/.

Verification

python docs/verify_lessons.py passes 23/23 against a fresh 0.5.0 build, and cargo test, cargo clippy --all-targets -- -D warnings and cargo fmt --check are clean. Every new code block in this PR was run, not just checked.

Best reviewed with whitespace off; the em dashes inside quoted compiler output are the compiler's own.