Zulip Chat Archive
Stream: maths
Topic: finsupp.to_module
Johan Commelin (Mar 26 2019 at 08:12):
Why is finsupp.to_module not an instance?
Chris Hughes (Mar 26 2019 at 13:28):
Because we never use finsupp as is, it's always renamed to something like polynomial or lc, and the instance wouldn't apply after it's renamed.
Johan Commelin (Mar 26 2019 at 13:28):
Ok, but it wouldn't hurt to make it an instance, right?
Chris Hughes (Mar 26 2019 at 13:30):
Probably not. There might be applications of finsupp where it really isn't a module. Why do you want it to be an instance?
Johan Commelin (Mar 26 2019 at 13:41):
Ooh, I don't necessarily want it to be a module. I was just curious about the reasoning behind the def.
Chris Hughes (Mar 26 2019 at 13:42):
It probably slightly slows down type class searches as well.
Scott Morrison (Mar 26 2019 at 19:35):
Let's err on the side of making nothing an instance that isn't really clearly needed. :-)
Last updated: Dec 20 2023 at 11:08 UTC