Zulip Chat Archive

Stream: triage

Topic: PR #2843: refactor(algebra/group/basic): minimal axioms f...


view this post on Zulip Random Issue Bot (Dec 06 2020 at 14:22):

Today I chose PR 2843 for discussion!

refactor(algebra/group/basic): minimal axioms for group and comm_monoid
Created by @Chris Hughes (@ChrisHughes24) on 2020-05-27
Labels: WIP, merge-conflict

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

view this post on Zulip Eric Wieser (Dec 06 2020 at 18:55):

Should we do this, but with auto_param for the redundant lemmas instead?


Last updated: May 18 2021 at 23:14 UTC