Skip to content

fix: disambiguate duplicate Verso labels across Chapter 3 - #657

Open
Chessing234 wants to merge 1 commit into
teorth:mainfrom
Chessing234:fix/chapter-3-verso-labels
Open

fix: disambiguate duplicate Verso labels across Chapter 3#657
Chessing234 wants to merge 1 commit into
teorth:mainfrom
Chessing234:fix/chapter-3-verso-labels

Conversation

@Chessing234

Copy link
Copy Markdown
Contributor

Ten groups of sibling declarations in Chapter 3 share a docstring:

Label File Count
Exercise 3.1.2 3.1 3
Lemma 3.1.12 (Basic properties of unions) / Exercise 3.1.3 3.1 3
Examples 3.1.16 3.1 2
Proposition 3.1.17 (Partial ordering by set inclusion) 3.1 3
Axiom 3.6 (axiom of specification) 3.1 3
Exercise 3.1.12. 3.1 3
Exercise 3.2.2, Exercise 3.2.3 3.2 2 each
Exercise 3.4.5, Exercise 3.4.11 3.4 2 each
Exercise 3.4.10 3.4 3
Definition 3.5.6 3.5 2

Same convention as #624: keep the statement number, name the case in the parenthetical — (commutativity), (antisymmetry), (complement of a union), and so on. #622 covered Exercises 3.5.4/3.5.5 and #638 Example 3.5.10; these are the remaining collisions in the chapter.

One extra: Exercise 3.1.12. carried a trailing full stop that no other label in the file has, so the three labels now read Exercise 3.1.12 (unions) etc. Docstrings only.

Checked: no duplicate one-line docstrings remain in any of the four files, all edited lines within 100 characters.

lake build of all four modules succeeds locally — Build completed successfully (3267 jobs).

Thirty docstrings in Sections 3.1-3.5 shared a label with a sibling
declaration, including Exercise 3.1.2, Lemma 3.1.12, Proposition 3.1.17,
Axiom 3.6, Exercise 3.1.12, Exercises 3.2.2/3.2.3, Exercises 3.4.5/3.4.10/
3.4.11 and Definition 3.5.6.

Each now names what it covers while keeping the statement number.  The stray
full stop in "Exercise 3.1.12." goes at the same time, so the three labels
match the numbering used everywhere else in the file.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant