Zulip Chat Archive
Stream: mathlib4
Topic: to_additive generates nonsense names for Prod instances
Eric Wieser (Mar 17 2023 at 12:41):
It seems the additive version of docs4#Prod.instOneProd is docs4#Prod.instZeroSum, where Sum is out of place. Is naming the instances explicitly by hand reasonable?
Jireh Loreaux (Mar 17 2023 at 12:51):
Are you porting tsze?
Eric Wieser (Mar 17 2023 at 12:51):
Yes
Eric Wieser (Mar 17 2023 at 12:51):
The PR it was waiting on is now merged
Jireh Loreaux (Mar 17 2023 at 12:52):
I noticed the weird names while porting unitization.
Jireh Loreaux (Mar 17 2023 at 12:54):
I think if you name them by hand then to_additive will translate the names for you. So manual naming makes sense. I've been trying to do that for instances anyway.
Eric Wieser (Mar 17 2023 at 13:50):
Jireh Loreaux (Mar 17 2023 at 14:10):
You'll have to manually change Unitization since I just used the bad names.
Last updated: Dec 20 2023 at 11:08 UTC