Skip to content

Conversation

jamesmckinna
Copy link
Contributor

@jamesmckinna jamesmckinna commented Jul 1, 2024

NB:

  • UPDATED: CHANGELOG added (but merge conflicts until v2.1 is released)
  • no public re-export of properties of (Commutative)Monoid inheriting from (Commutative)Semigroup (and perhaps this is a downstream issue to rationalise the hierarchy of Algebra.Properties.* to better reflect such inheritance hierarchies...?)
  • knock-on consequences for Refactor Algebra.Solver.*Monoid #2407 /downstream (whether or not this is merged first)...

Additionally (but out of scope here):

  • possible other [DRY] redundancies/refactoring opportunities exposed in Algebra.Properties.CommutativeSemigroup and elsewhere (eg. the semimedial properties are all instances of interchange; the pattern sym (assoc x y z) is already defined by Algebra.Properties.Semigroup.x∙yz≈xy∙z etc.)

@jamesmckinna jamesmckinna added this to the v2.2 milestone Jul 1, 2024
@jamesmckinna jamesmckinna linked an issue Jul 1, 2024 that may be closed by this pull request
@jamesmckinna jamesmckinna added this pull request to the merge queue Aug 2, 2024
Merged via the queue into agda:master with commit a162b5c Aug 2, 2024
@jamesmckinna jamesmckinna deleted the issue2408 branch August 12, 2024 08:30
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Add Algebra.Properties.IdempotentCommutativeMonoid
3 participants