Skip to content

[Merged by Bors] - fix(to_additive): automatically translate all instances generated by extends#19302

Closed
fpvandoorn wants to merge 4 commits intomasterfrom
to_additive_extends
Closed

[Merged by Bors] - fix(to_additive): automatically translate all instances generated by extends#19302
fpvandoorn wants to merge 4 commits intomasterfrom
to_additive_extends

Conversation

@fpvandoorn
Copy link
Copy Markdown
Member

@fpvandoorn fpvandoorn commented Nov 20, 2024 •
edited by Ruben-VandeVelde
Loading

Fixes #660

Open in Gitpod

@fpvandoorn fpvandoorn added help-wanted The author needs attention to resolve issues awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. labels Nov 20, 2024
@github-actions
Copy link
Copy Markdown

github-actions bot commented Nov 20, 2024 •
edited
Loading

PR summary f7242f8189

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

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.

Decrease in tech debt: (relative, absolute) = (2.00, 0.00)
Current number Change Type
5086 -2 porting notes

Current commit f7242f8189
Reference commit 8e0d70c35d

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).

@fpvandoorn fpvandoorn mentioned this pull request Nov 20, 2024
Open
20 tasks
@github-actions github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Nov 20, 2024
@fpvandoorn fpvandoorn removed the help-wanted The author needs attention to resolve issues label Nov 20, 2024
@grunweg grunweg added the t-meta Tactics, attributes or user commands label Dec 7, 2024
@alexjbest
Copy link
Copy Markdown
Member

alexjbest commented Dec 21, 2024

maintainer merge

@github-actions
Copy link
Copy Markdown

github-actions bot commented Dec 21, 2024

🚀 Pull request has been placed on the maintainer queue by alexjbest.

@github-actions github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Dec 21, 2024
@kmill
Copy link
Copy Markdown
Contributor

kmill commented Dec 21, 2024

Thanks! (I should have merged this long ago, sorry! Nice to see the parent info being used :-))

bors r+

@ghost ghost added the ready-to-merge This PR has been sent to bors. label Dec 21, 2024
mathlib-bors bot pushed a commit that referenced this pull request Dec 21, 2024
@fpvandoorn @Ruben-VandeVelde
fix(to_additive): automatically translate all instances generated by …
c459ca0 
…`extends` (#19302)

Fixes  #660



Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Dec 22, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title fix(to_additive): automatically translate all instances generated by extends [Merged by Bors] - fix(to_additive): automatically translate all instances generated by extends Dec 22, 2024
@mathlib-bors mathlib-bors bot closed this Dec 22, 2024
@mathlib-bors mathlib-bors bot deleted the to_additive_extends branch December 22, 2024 00:41
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. ready-to-merge This PR has been sent to bors. t-meta Tactics, attributes or user commands

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

to_additive unable to translate toOneHomClass

5 participants

@fpvandoorn @alexjbest @kmill @grunweg @Ruben-VandeVelde