Zulip Chat Archive

Stream: mathlib4

Topic: More to_additive issues


Richard Osborn (Nov 28 2022 at 00:24):

While porting Algebra.Regular.Basic (mathlib4#758), to_additive has not been finding the correct translations. I can fix most of the problems by giving an explicit name for the additive version of IsLeftRegular and IsRightRegular, but roughly 9 theorems still fail. Should those be duplicated manually for now or is there an easy fix to to_additive? I'm not really sure how to debug such things.

Damiano Testa (Nov 28 2022 at 00:35):

Hi, I think that I was the author of the file. When I added the to_additive conversion, I also added a dictionary entry to to_additive to convert regular to add_regular and the left/right variants. I cannot see now how to do a similar change for the mathlib4 version of to_additive, but hopefully this explains why the attribute does not find the right name.

Damiano Testa (Nov 28 2022 at 00:46):

I'm on mobile, so I cannot help much, but these are the mathlib lines that I added:

https://github.com/leanprover-community/mathlib/blob/master/src/tactic/to_additive.lean#L226-L229

Jireh Loreaux (Nov 28 2022 at 01:37):

Side note: @Richard Osborn just FYI: you marked Algebra.Regular.Basic with a Yes on the port status wiki. The Yes is reserved for PRs that have already been merged, and marking it too early could cause issues. It's not a big deal, I've already fixed it, I'm just informing.


Last updated: Dec 20 2023 at 11:08 UTC