fix: disambiguate Verso labels in Section 9.1

[Chessing234]

Summary

• Split duplicate Verso exercise doc labels in Section 9.1 so each exercise part has a unique label for the HTML build.

Test plan

• CI / docs build passes
• Spot-check Section 9.1 exercise anchors in the rendered book

Made with Cursor

[teorth]

Thanks for the careful work here — but I'm going to decline this one, because the premise doesn't hold for this repo.

Repeated identical exercise docstrings are intentional house style, not a build hazard. They appear throughout: 12x /-- Exercise 5.4.9 -/, 6x /-- Exercise 3.5.4 -/, 6x /-- Exercise 3.1.7 -/, and many more. There is no label or anchor machinery keyed on docstring text — literate.toml sets docstrings_as_text = true, so docstrings render as plain text and book anchors come from declaration names. The book has been building and deploying with these duplicates all along, which is also why CI is green on these PRs: there was nothing to fix.

The added parentheticals also introduce part-labels that aren't in the textbook (e.g. Definition 6.1.3 (ε-steady, def), Definition 6.1.8 (lim, characterization)), which risks reading as though the text has parts it doesn't.

If you'd like to propose changing this convention, please open an issue first — it should be settled repo-wide rather than section by section.

The contributions I'm most glad to receive are the ones you've been sending: corrections to sorryd statements that are false or mis-hypothesized, in the spirit of #517. Those have been genuinely valuable.

[teorth]

Reopening — please disregard my previous comment, which was wrong.

I assessed this against a stale checkout of main that was roughly 200 commits behind origin/main. The duplicate-docstring counts I cited (12x /-- Exercise 5.4.9 -/ and so on) were from that stale tree; those had already been fixed on main by #616 and the other label PRs. The label-disambiguation work is an active and accepted cleanup here, not a departure from house style, and this PR is a legitimate continuation of it.

Apologies for the noise.