Zulip Chat Archive
Stream: general
Topic: to_additive attribute order
Reid Barton (Sep 07 2020 at 17:01):
If there are other attributes on a definition which I want to_additive to copy to the additive version, then to_additive should come last, right? Or does it not matter?
Reid Barton (Sep 07 2020 at 17:01):
I didn't see anything about this in the documentation.
Chris Hughes (Sep 07 2020 at 17:51):
Yes, to_additive adds simp and some other attributes (but not all) to the generated declarations.
Reid Barton (Sep 08 2020 at 00:10):
I tested and you do need to put other attributes first if you want them to be copied.
Yaël Dillies (Apr 27 2022 at 20:48):
Is the attribute order documented anywhere? I found yet another interaction that can go wrong:to_additive and norm_cast. docs#continuous_map.coe_smul gets it wrong.
Alex J. Best (Apr 27 2022 at 20:53):
I don't think the order is documented but the rule is always put to additive last, unless it complains, in which case do what the error message says.
Yaël Dillies (Apr 27 2022 at 20:53):
... except simps
Alex J. Best (Apr 27 2022 at 20:53):
Things slip through the cracks of course and I try and do a grep search and fix things occasionally, but that is also imperfect.
Alex J. Best (Apr 27 2022 at 20:54):
Well that comes under the unless it complains branch of my rule
Alex J. Best (Apr 27 2022 at 20:54):
Simps and mono are the only exceptions iirc but the user doesn't really have to remember that
Yaël Dillies (Apr 27 2022 at 20:54):
and is there any other interaction between norm_cast, simp and others?
Alex J. Best (Apr 27 2022 at 20:55):
I don't think they interact, but I'm not 100% sure
Yaël Dillies (Apr 27 2022 at 20:58):
I know for a fact that to_additive and alias interact (in bad ways), but #13742 and #13743 should fix this.
Alex J. Best (Apr 27 2022 at 21:09):
Yes most attribute pairs don't interact though. to_additive is one of the few attributes that creates a new declaration that needs attributes of it's own, so more care is needed
Damiano Testa (Apr 28 2022 at 01:33):
I don't really understand how to_additive does its magic, but I've looked at the code a few times. It seems that
is where there is (at least part of) the handling of attributes. You can also see that simps, mono and something with alias get singled out.
Last updated: Dec 20 2023 at 11:08 UTC