Skip to content

[Merged by Bors] - feat: use to_additive for Monoid.End#19687

Closed
fpvandoorn wants to merge 14 commits intomasterfrom
dont_translate_hom
Closed

[Merged by Bors] - feat: use to_additive for Monoid.End#19687
fpvandoorn wants to merge 14 commits intomasterfrom
dont_translate_hom

Conversation

@fpvandoorn
Copy link
Copy Markdown
Member

@fpvandoorn fpvandoorn commented Dec 2, 2024 •
edited by alreadydone
Loading

  • Rename Monoid.coe_one and Monoid.coe_mul to Monoid.End.coe_one and Monoid.End.coe_mul, which is already the name for AddMonoid.End. I made the deprecations protected in order to not cause overloading issues.
  • Change some instance names to increase consistency in names (no deprecations added)

Open in Gitpod

@fpvandoorn fpvandoorn mentioned this pull request Dec 2, 2024
Closed
@github-actions
Copy link
Copy Markdown

github-actions bot commented Dec 2, 2024 •
edited
Loading

PR summary ff9a29aad5

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ MonoidHom.instCommGroup
+ MonoidHom.instCommMonoid
+ instMonoid
- End
- MonoidHom.commGroup
- MonoidHom.commMonoid
- coe_pow
- instAddMonoidHomClass
- instFunLike
- instMul
- instOne
- instance : Inhabited (AddMonoid.End A) := ⟨1⟩
- instance : Monoid (Monoid.End M)
- monoid

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 relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
  • The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Dec 2, 2024
mathlib-bors bot pushed a commit that referenced this pull request Dec 22, 2024
@fpvandoorn
feat(to_additive): option to not translate operations on a type (#19297)
2f4156e 
* Also some cleanup in the `ToAdditive/Frontend` file (please review the first 3 commits separately), only the second commit actually changes the functionality of `to_additive`. The main cleanups: move doc-strings to the syntax declarations, remove the module doc which was just duplicating the `to_additive`-doc, and let a few internal functions depend on `Environment` instead of multiple other arguments.
* In #19687 this is done for `Monoid.End` (in a separate PR, since that requires some library fixes).
@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Dec 22, 2024
@mathlib4-dependent-issues-bot
Copy link
Copy Markdown
Collaborator

mathlib4-dependent-issues-bot commented Dec 22, 2024

This PR/issue depends on:

@fpvandoorn fpvandoorn changed the title feat: to_additive doesn't translate operations on Monoid.End feat: use to_additive for Monoid.End Dec 23, 2024
jcommelin
jcommelin reviewed Jan 20, 2025
View reviewed changes
Copy link
Copy Markdown
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks 🎉

bors merge

@ghost ghost added the ready-to-merge This PR has been sent to bors. label Jan 20, 2025
mathlib-bors bot pushed a commit that referenced this pull request Jan 20, 2025
@fpvandoorn
feat: use to_additive for Monoid.End (#19687)
06cfa2a 
* Rename `Monoid.coe_one` and `Monoid.coe_mul` to `Monoid.End.coe_one` and `Monoid.End.coe_mul`, which is already the name for `AddMonoid.End`. I made the deprecations `protected` in order to not cause overloading issues.
* Change some instance names to increase consistency in names (no deprecations added)
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jan 20, 2025

Build failed (retrying...):

mathlib-bors bot pushed a commit that referenced this pull request Jan 20, 2025
@fpvandoorn
feat: use to_additive for Monoid.End (#19687)
b823988 
* Rename `Monoid.coe_one` and `Monoid.coe_mul` to `Monoid.End.coe_one` and `Monoid.End.coe_mul`, which is already the name for `AddMonoid.End`. I made the deprecations `protected` in order to not cause overloading issues.
* Change some instance names to increase consistency in names (no deprecations added)
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jan 20, 2025

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: use to_additive for Monoid.End [Merged by Bors] - feat: use to_additive for Monoid.End Jan 20, 2025
@mathlib-bors mathlib-bors bot closed this Jan 20, 2025
@mathlib-bors mathlib-bors bot deleted the dont_translate_hom branch January 20, 2025 16:37
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@jcommelin jcommelin jcommelin left review comments

Assignees

No one assigned

Labels

ready-to-merge This PR has been sent to bors.

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@fpvandoorn @mathlib4-dependent-issues-bot @jcommelin