-
Notifications
You must be signed in to change notification settings - Fork 330
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - chore: split Data.Set.Basic #18317
Conversation
PR summary 4d877d4c3c
|
File | Base Count | Head Count | Change |
---|---|---|---|
Mathlib.Data.Set.Basic | 213 | 194 | -19 (-8.92%) |
Mathlib.Data.SetLike.Basic | 216 | 197 | -19 (-8.80%) |
Mathlib.Order.Filter.Defs | 216 | 197 | -19 (-8.80%) |
Mathlib.Order.Interval.Set.Basic | 220 | 202 | -18 (-8.18%) |
Mathlib.Data.PEquiv | 217 | 200 | -17 (-7.83%) |
Mathlib.Algebra.Group.Center | 233 | 215 | -18 (-7.73%) |
Mathlib.Data.Set.Enumerate | 333 | 332 | -1 (-0.30%) |
Mathlib.Data.PNat.Basic | 422 | 421 | -1 (-0.24%) |
Import changes for all files
Files | Import difference |
---|---|
There are 4202 files with changed transitive imports taking up over 177914 characters: this is too many to display! | |
You can run scripts/import_trans_difference.sh all locally to see the whole output. |
Declarations diff
No declarations were harmed in the making of this PR! 🐙
You can run this locally as follows
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>
The doc-module for script/declarations_diff.sh
contains some details about this script.
Thanks 🎉 If CI passes, please remove the label bors d+ |
✌️ kim-em can now approve this pull request. To approve and merge a pull request, simply reply with |
bors merge |
Delay imports of `Data.Order.SymmDiff`, as many things downstream don't need it.
Pull request successfully merged into master. Build succeeded: |
Delay imports of
Data.Order.SymmDiff
, as many things downstream don't need it.