Zulip Chat Archive

Stream: general

Topic: have `ring` fall back to `noncomm_ring`?


view this post on Zulip Scott Morrison (May 31 2020 at 07:06):

Now that we have a basic version of noncomm_ring available (that just calls simp with an appropriate simpset, then abel), could we arrange so that ring falls back to noncomm_ring when it can't find an appropriate comm_semiring instance?

view this post on Zulip Scott Morrison (May 31 2020 at 07:06):

I had a bit of a look through ring, but couldn't work out how to do this.

view this post on Zulip Mario Carneiro (May 31 2020 at 07:32):

ring already has fallback behavior, and it also doesn't a priori know what type it is working over, so not finding a comm_ring instance is possibly not a failure. All of which makes it difficult to use noncomm_ring as backup. Plus this is always going to be slower than calling noncomm_ring directly.

view this post on Zulip Mario Carneiro (May 31 2020 at 07:33):

That is, there are valid uses of ring when applied to an equality of non-commutative rings. Currently ring will act as a normalizer on any embedded subterms that are in commutative rings


Last updated: May 15 2021 at 23:13 UTC