Conversation
PR summary 757a4e6a0f
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.Data.ENat.Basic | 477 | 476 | -1 (-0.21%) |
Import changes for all files
| Files | Import difference |
|---|---|
8 filesMathlib.Combinatorics.SimpleGraph.Diam Mathlib.Combinatorics.SimpleGraph.Metric Mathlib.Data.ENat.Basic Mathlib.Data.ENat.BigOperators Mathlib.Data.ENat.Lattice Mathlib.NumberTheory.Padics.PadicVal.Defs Mathlib.Order.Height Mathlib.RingTheory.Multiplicity |
-1 |
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.
No changes to technical debt.
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).
|
bot fix style |
adomani
left a comment
There was a problem hiding this comment.
This comment came from a review
bot fix style
bot fix style
and I wrote bot fix style twice (or is it 3 times?).
0fdec63 to
062fb9d
Compare
adomani
left a comment
There was a problem hiding this comment.
Even without the prompt of the bot, I will still say
bot fix style
in a review.
adomani
left a comment
There was a problem hiding this comment.
From review
bot fix style
| types: [created, edited] | ||
| pull_request_review: | ||
| # triggers on a review, whether or not it is accompanied by a comment | ||
| types: [submitted] |
There was a problem hiding this comment.
From review comment
bot fix style
There was a problem hiding this comment.
The above comment worked, but reviewdog had not posted anything.
…y/mathlib4 into test/merge_bot_fixes
adomani
left a comment
There was a problem hiding this comment.
From review
bot fix style
|
Thanks for your help in debugging! |
A PR accompanying #20789.