Zulip Chat Archive

Stream: triage

Topic: PR #11782: feat(algebra/order/monoid_lemmas_pos): use `co...


Random Issue Bot (Mar 01 2022 at 14:13):

Today I chose PR 11782 for discussion!

feat(algebra/order/monoid_lemmas_pos): use co(ntra)variant_class with positive elements
Created by @damiano (@adomani) on 2022-02-02
Labels: RFC

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

Damiano Testa (Mar 01 2022 at 16:26):

This PR was simply a show-case of some of the lemmas to come. A PR along these lines is already merge (#11833) and another one is open (#12355).

At this point, the PR mentioned by the bot could be closed. However, I may wait until the #12355 receives some comments, before closing this one.

Random Issue Bot (May 05 2022 at 14:21):

Today I chose PR 11782 for discussion!

feat(algebra/order/monoid_lemmas_pos): use co(ntra)variant_class with positive elements
Created by @damiano (@adomani) on 2022-02-02
Labels: RFC

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

Damiano Testa (May 05 2022 at 17:10):

This is on its way: @FR is helping with the refactor and lemmas and instances are moving!


Last updated: Dec 20 2023 at 11:08 UTC