[Merged by Bors] - chore: change the definition of List.finRange#19447
[Merged by Bors] - chore: change the definition of List.finRange#19447
List.finRange#19447Conversation
PR summary c25fea8a05Import changes exceeding 2%
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.Data.List.Range | 339 | 287 | -52 (-15.34%) |
| Mathlib.Data.List.Sublists | 345 | 354 | +9 (+2.61%) |
| Mathlib.Data.List.FinRange | 351 | 348 | -3 (-0.85%) |
Import changes for all files
| Files | Import difference |
|---|---|
Mathlib.Data.List.Range |
-52 |
Mathlib.Data.List.FinRange |
-3 |
Mathlib.Data.Finset.Powerset |
5 |
Mathlib.Algebra.BigOperators.Ring.Multiset |
8 |
3 filesMathlib.Data.Multiset.Antidiagonal Mathlib.Data.List.Sublists Mathlib.Data.Multiset.Powerset |
9 |
Declarations diff
+ finRange_eq_pmap_range
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.
Increase in tech debt: (relative, absolute) = (1.00, 0.01)
| Current number | Change | Type |
|---|---|---|
| 184 | 1 | adaptation notes |
Current commit c25fea8a05
Reference commit b96544419e
You can run this locally as
./scripts/technical-debt-metrics.sh pr_summary
- The
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
|
|
||
| /- #adaptation_note: this attribute should be removed after Mathlib moves to v4.15.0-rc1. -/ | ||
| set_option allowUnsafeReducibility true in | ||
| attribute [semireducible] Fin.foldr.loop |
There was a problem hiding this comment.
Does this apply globally, or just for the current file?
There was a problem hiding this comment.
I also worry that this PR might have accumulated a bunch of proof uglification before we discovered this fix; is that the case, or do I have the chronology wrong?
There was a problem hiding this comment.
The uglification seems to still be necessary at the moment, and I'm not really sure why it is happening. It is only at the level of having to redo some simp only blocks, however.
There was a problem hiding this comment.
Does this apply globally, or just for the current file?
This is global.
jcommelin
left a comment
There was a problem hiding this comment.
Thanks 🎉
If CI passes, please remove the label awaiting-CI and merge this yourself, by adding a comment bors r+.
bors d+
|
✌️ kim-em can now approve this pull request. To approve and merge a pull request, simply reply with |
|
bors merge |
François Dorais has been [working](leanprover-community/batteries#1055) on upstreaming `List.finRange`, but wants to change the definition at the same time. That was running into difficulties, which hopefully are resolved here.
|
Pull request successfully merged into master. Build succeeded: |
List.finRangeList.finRange
François Dorais has been working on upstreaming
List.finRange, but wants to change the definition at the same time. That was running into difficulties, which hopefully are resolved here.