[Merged by Bors] - chore: more simpNF cleanup#19395
Conversation
PR summary 5f7bf84551Import changes for modified filesNo significant changes to the import graph Import changes for all files
|
| Current number | Change | Type |
|---|---|---|
| 5060 | -25 | porting notes |
| 207 | -14 | disabled simpNF lints |
Current commit 5f7bf84551
Reference commit 43c93172bd
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).
Mathlib/NumberTheory/Modular.lean
Outdated
|
|
||
| -- `simpNF` times out, but only in CI where all of `Mathlib` is imported | ||
| attribute [nolint simpNF] lcRow0Extend_apply lcRow0Extend_symm_apply | ||
| -- attribute [nolint simpNF] lcRow0Extend_apply lcRow0Extend_symm_apply |
There was a problem hiding this comment.
Still checking in CI.
There was a problem hiding this comment.
It looks like CI liked the change!
adomani
left a comment
There was a problem hiding this comment.
Thanks: this looks good to me!
bors d+
Mathlib/NumberTheory/Modular.lean
Outdated
|
|
||
| -- `simpNF` times out, but only in CI where all of `Mathlib` is imported | ||
| attribute [nolint simpNF] lcRow0Extend_apply lcRow0Extend_symm_apply | ||
| -- attribute [nolint simpNF] lcRow0Extend_apply lcRow0Extend_symm_apply |
There was a problem hiding this comment.
It looks like CI liked the change!
|
✌️ kim-em can now approve this pull request. To approve and merge a pull request, simply reply with |
|
bors merge |
|
Pull request successfully merged into master. Build succeeded: |
No description provided.