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

Stream: triage

[Random Issue Bot]

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]

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]

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]

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