Zulip Chat Archive

Stream: triage

Topic: issue #2534: Get rid of `is_(semi)ring_hom`

view this post on Zulip Random Issue Bot (Apr 15 2021 at 14:23):

Today I chose issue 2534 for discussion!

Get rid of is_(semi)ring_hom
Created by @Yury G. Kudryashov (@urkud) on 2020-04-25
Labels: needs-refactor

Is this issue still relevant? Any recent updates? Anyone making progress?

view this post on Zulip Kevin Buzzard (Apr 15 2021 at 14:56):

I am still confused by the goal here, and my memory is also sufficiently bad that I can never remember which is which out of is_blah_hom and is_subblah we want to keep. Both? Is the idea to delete is_subblah completely and refactor, or is the idea just to turn these things from classes to structures?

view this post on Zulip Anne Baanen (Apr 15 2021 at 15:15):

IIRC, we want to keep both is_blah_hom and is_subblah as structures.

view this post on Zulip Eric Wieser (Apr 15 2021 at 16:18):

Didn't your experiments conclude we also want a blam_hom_class?

Last updated: May 09 2021 at 16:20 UTC