fix: disambiguate remaining duplicate Verso labels in Chapters 2, 5 and 9 - #658
fix: disambiguate remaining duplicate Verso labels in Chapters 2, 5 and 9#658Chessing234 wants to merge 2 commits into
Conversation
…nd 9 Twenty-one docstrings across nine groups shared a label with a sibling: Proposition 2.1.16, Proposition 2.3.6, Definition 2.3.11, Example 5.1.10, Definition 5.1.12, Definitions 5.2.3 and 5.2.6, the Example 5.5.2 API, and Examples 9.3.4 and 9.3.5. Definitions and propositions name the case in the parenthetical; the examples take part letters.
|
Thanks — the great majority of this is exactly right, and I've merged the sibling label PRs using the same descriptive style. Two changes here I'd like adjusted before merging: the
and 9.3.5 is the same statement about Descriptive parentheticals in the style you've used elsewhere in this PR would work well, e.g. Everything else in the PR — the 2.1.16, 2.3.6, 2.3.11, 5.1.12, 5.2.3, 5.2.6 and 5.5.2 disambiguators — is good as-is. |
Both are single-paragraph example environments in ch9 with no enumerated parts, so (a)/(b) pointed at parts a reader cannot find. Describe the two cases instead, matching the style used elsewhere in this PR.
|
Done in a8fc2e7. Both pairs now describe the case rather than a part number: |
2 participants
The label collisions left in Chapters 2, 5 and 9 after #616, #624, #626, #634 and the Section 5.3/5.6 PRs:
Proposition 2.1.16 (recursive definitions).Proposition 2.3.6 (Multiplication preserves order)Definition 2.3.11 (Exponentiation for natural numbers)Example 5.1.10.Definition 5.1.12 (bounded sequences)Definition 5.2.3 (Eventually ε-close sequences)Definition 5.2.6 (Equivalent sequences)API for Example 5.5.2Example 9.3.4,Example 9.3.5Same convention as #624: definitions and propositions name the case in the parenthetical, examples take part letters (#634). Docstrings only.
Note on Section 2.2: it has two labels of the form
(d) (Addition preserves order). Compare with Mathlib's {name}Nat.add_le_add_right`` that differ only in the Mathlib name they cite, so they are already distinct — left alone.Checked: no duplicate one-line docstrings remain in any of the six files, all edited lines within 100 characters.
lake buildof all six modules succeeds locally —Build completed successfully (3282 jobs).