Add `Algebra.Properties.IdempotentCommutativeMonoid` #2408

Closed

Closed

Add Algebra.Properties.IdempotentCommutativeMonoid#2408

Labels

additionrefactoring

Milestone

opened

on Jun 14, 2024

· edited by jamesmckinna

Contributor

Cf. #2138 / #2402 as well as #2403 / #2407 together with

Algebra.Properties.IsBand
etc.
Eg Algebra.Solver.IdempotentCommutativeMonoid.distr could/should be lifted out ... what else though?

added

on Jun 14, 2024

added a commit that references this issue

fixes agda#2408

linked a pull request that will close this issuefixes #2408 #2422

added this to the v2.2 milestone

github-merge-queue

added a commit that references this issue

fixes #2408 (#2422)

closed this as completedin #2422

to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Assignees

No one assigned

Labels

additionrefactoring

Type

No type

Projects

No projects

Milestone

v2.2
Closed Jan 22, 2025, 100% complete

Relationships

None yet

Development

fixes #2408agda/agda-stdlib

Participants