Random Issue Bot (Apr 15 2021 at 14:23):
Today I chose issue 2534 for discussion!
Get rid of
Created by @Yury G. Kudryashov (@urkud) on 2020-04-25
Is this issue still relevant? Any recent updates? Anyone making progress?
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_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?
Anne Baanen (Apr 15 2021 at 15:15):
IIRC, we want to keep both
is_subblah as structures.
Eric Wieser (Apr 15 2021 at 16:18):
Didn't your experiments conclude we also want a
Last updated: May 09 2021 at 16:20 UTC