Random Issue Bot (Jan 08 2021 at 14:32):
Today I chose PR 5010 for discussion!
feat(data/fin): identities in add and mul monoids
Created by @Yakov Pechersky (@pechersky) on 2020-11-15
Labels: WIP, awaiting-author, merge-conflict
Is this PR still relevant? Any recent updates? Anyone making progress?
Yakov Pechersky (Jan 08 2021 at 14:50):
I'd like to make this PR something about transferring the
comm_ring instance or some substructure of that for
fin out of
data/fin. That way there wouldn't have to be "orphan"
add_assoc and the like. I understand that one shouldn't be doing "add" or "mul" in
fin, but at least given the definitions we have now, it's very hard to deal with these operations when they appear. A compromise might be to just have
add_group and nothing more.
Last updated: May 09 2021 at 16:20 UTC