Skip to content

fix: Ex. 1.2.18/1.2.24 duplicate doc labels - #574

Merged
teorth merged 1 commit into
teorth:mainfrom
Chessing234:fix/measure-1-2-18-24-exercise-labels
Aug 2, 2026
Merged

fix: Ex. 1.2.18/1.2.24 duplicate doc labels#574
teorth merged 1 commit into
teorth:mainfrom
Chessing234:fix/measure-1-2-18-24-exercise-labels

Conversation

@Chessing234

@Chessing234 Chessing234 commented Jul 8, 2026

Copy link
Copy Markdown
Contributor

Summary

  • Renumber second Exercise 1.2.18(ii) (inner_measure.eq_iff) to (iii).
  • Drop duplicate (ii) labels on Ex. 1.2.24 metric/complete instances.
  • Split duplicate Exercise 1.2.12 (i/ii) and 1.2.22 (i–iii) labels.

Test plan

  • lake build Analysis.MeasureTheory.Section_1_2_2

Rebased onto upstream/main; disambiguate repeated exercise labels.

Co-authored-by: Cursor <cursoragent@cursor.com>
@Chessing234
Chessing234 force-pushed the fix/measure-1-2-18-24-exercise-labels branch from 989399d to 59f8d28 Compare July 29, 2026 15:43
@Chessing234

Copy link
Copy Markdown
Contributor Author

@teorth gentle bump — this is a small Verso/docstring hygiene fix with green CI. Happy to rebase or adjust if anything looks off; otherwise ready whenever you have a moment.

@teorth
teorth merged commit 8d0706c into teorth:main Aug 2, 2026
2 checks passed
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.

2 participants