Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

to_additive guesses a bad name in some edge cases #9945

Closed
robertylewis opened this issue Oct 24, 2021 · 2 comments
Closed

to_additive guesses a bad name in some edge cases #9945

robertylewis opened this issue Oct 24, 2021 · 2 comments

Comments

@robertylewis
Copy link
Member

I just noticed the misnamed, auto-generated add_subgroup.card_nonpos_iff_eq_bot in #9918 . Who maintains to_additive? I'll look myself if/when I find time, but this isn't a top priority.
@fpvandoorn
Copy link
Member

@[to_additive] would need major new features for it to recognize this automatically. I think it's just the responsibility of the user in cases like these to give the correct additive name.

@robertylewis robertylewis mentioned this issue Nov 9, 2021
Closed
@semorrison semorrison mentioned this issue Mar 8, 2023
Closed
@semorrison
Copy link
Collaborator

I agree this is out of scope of automation for now, so will just close this.

bors bot pushed a commit to leanprover-community/mathlib4 that referenced this issue Mar 8, 2023
@semorrison
chore: fix some bad names generated by to_additive (#2706)
3f960e3 
These were noticed back in leanprover-community/mathlib#9945 but never fixed. It seems unlikely that we're ever going to make `to_additive` smart enough to cope here by itself.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
3 participants
@semorrison @robertylewis @fpvandoorn