Zulip Chat Archive

Stream: maths

Topic: finsupp.to_module


view this post on Zulip Johan Commelin (Mar 26 2019 at 08:12):

Why is finsupp.to_module not an instance?

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Mar 26 2019 at 13:28):

Ok, but it wouldn't hurt to make it an instance, right?

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Chris Hughes (Mar 26 2019 at 13:42):

It probably slightly slows down type class searches as well.

view this post on Zulip 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