Zulip Chat Archive
Stream: general
Topic: Funny error by to_additive
Brendan Seamas Murphy (Aug 26 2022 at 00:33):
image.png
What exactly is a "neg_fun"? :thinking:
Adam Topaz (Aug 26 2022 at 01:35):
A biproduct of to_additive?
Adam Topaz (Aug 26 2022 at 01:35):
Adam Topaz (Aug 26 2022 at 01:36):
yeah, I guess to_additive blindly replaced inv with neg.
Last updated: May 02 2025 at 03:31 UTC