Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Add Algebra.Properties.IdempotentCommutativeMonoid #2408

Closed
jamesmckinna opened this issue Jun 14, 2024 · 0 comments · Fixed by #2422
Closed

Add Algebra.Properties.IdempotentCommutativeMonoid #2408

jamesmckinna opened this issue Jun 14, 2024 · 0 comments · Fixed by #2422
Labels
addition refactoring
Milestone
v2.2

Comments

@jamesmckinna
Copy link
Contributor

jamesmckinna commented Jun 14, 2024 •
edited
Loading

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?
jamesmckinna added a commit to jamesmckinna/agda-stdlib that referenced this issue Jul 1, 2024
@jamesmckinna
fixes agda#2408
cc6a8e7
@jamesmckinna jamesmckinna linked a pull request Jul 1, 2024 that will close this issue
fixes #2408 #2422
Merged
@jamesmckinna jamesmckinna added this to the v2.2 milestone Jul 8, 2024
github-merge-queue bot pushed a commit that referenced this issue Aug 2, 2024
@jamesmckinna
fixes #2408 (#2422)
a162b5c 
* fixes #2408

* 'better' names?

* added `CHANGELOG` entry
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
addition refactoring
Projects
None yet
Milestone
v2.2
Development

Successfully merging a pull request may close this issue.

fixes #2408 jamesmckinna/agda-stdlib
1 participant
@jamesmckinna