chore(Mathlib/CategoryTheory/EffectiveEpi/Preserves.lean): automated extraction#37451
Conversation
PR summary 9799a64976
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.CategoryTheory.EffectiveEpi.Preserves | 592 | 593 | +1 (+0.17%) |
Import changes for all files
| Files | Import difference |
|---|---|
Mathlib.CategoryTheory.EffectiveEpi.Preserves |
1 |
Declarations diff
+ regularEpiOfPreserves
You can run this locally as follows
## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.
No changes to technical debt.
You can run this locally as
./scripts/reporting/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).
|
Thanks! maintainer delegate (I am not sure about the delegation mechanism on a spliced pr like this, this should be delegated to @dagurtomas ) |
|
🚀 Pull request has been placed on the maintainer queue by robin-carlier. |
mathlib-triage
bot
added
the
maintainer-merge
|
Also spliced PRs should get better PR titles. Perhaps there should be an argument to the splicing command? |
|
bors delegate @dagurtomas |
mathlib-triage
bot
added
delegated
|
bors d+ @dagurtomas |
|
✌️ mathlib-splicebot[bot] can now approve this pull request. To approve and merge a pull request, simply reply with |
|
Sorry, I don't remember the syntax, let me retry. bors delegate=[@dagurtomas ] |
|
bors delegate=dagurtomas |
|
✌️ dagurtomas can now approve this pull request. To approve and merge a pull request, simply reply with |
4 participants
This PR was automatically created from PR #37449 by @dagurtomas via a review comment by @dagurtomas.