Johan Commelin (Mar 26 2019 at 08:12):
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
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: May 11 2021 at 15:12 UTC