11 Pull requests merged by 7 people

• Cosmetics: delete 2 rewrite steps that do not fire

  #2758 merged Jul 3, 2025

• [ refactor ] Restate, and use, the definitions of Monotonic etc. operations

  #2580 merged Jul 3, 2025

• [Add] Consequences of associativity for Semigroups

  #2688 merged Jul 2, 2025

• Lemmata for if_then_else_

  #2747 merged Jul 2, 2025

• Proved sorted permutations are equal

  #2748 merged Jul 2, 2025

• Adds Algebra.Morphism.Construct.DirectProduct

  #2715 merged Jul 2, 2025

• Refactor Data.Vec.Properties : Add toList-injective and new lemmas

  #2733 merged Jun 30, 2025

• added insertion sort and refactored merge sort

  #2751 merged Jun 30, 2025

• Switch to Agda 2.8.0-rc3 by merging experimental into master

  #2755 merged Jun 30, 2025

• [ add ] Relation.Nullary.Decidable.dec-yes-recompute

  #2738 merged Jun 30, 2025

• Some extra support for homogeneous n-ary products

  #2736 merged Jun 30, 2025

2 Pull requests opened by 2 people

• Add instances of `IsString (List Char)`

  #2756 opened Jun 30, 2025

• `∸-suc` lemma for natural numbers

  #2757 opened Jul 1, 2025

11 Unresolved conversations

Sometimes conversations happen on old items that aren’t yet closed. Here is a list of all the Issues and Pull Requests with unresolved conversations.

• [ refactor ] (more) decidable `Data.Fin.Properties`

  #2744 commented on Jul 3, 2025 • 9 new comments

• Add `Algebra.Action.*` and friends

  #2350 commented on Jul 3, 2025 • 8 new comments

• [ refactor ] `Data.Fin.Properties` of decidable equality, plus knock-ons

  #2740 commented on Jul 3, 2025 • 6 new comments

• [Add] Consequences of identity for `monoids`

  #2692 commented on Jul 6, 2025 • 5 new comments

• [ add ] Choudhury and Fiore's alternative definition of `Permutation` for `Setoid`s

  #2726 commented on Jul 3, 2025 • 2 new comments

• `IsString` typeclass isn't actually listed as an instance in `Data.List.Literals`

  #2745 commented on Jun 30, 2025 • 0 new comments

• Fragile `NonZero` and implementation-dependent luck

  #2644 commented on Jul 2, 2025 • 0 new comments

• [ deprecate ] `Relation.Nullary.Reflects` and [ refactor ] `Relation.Nullary.Decidable.Core`

  #2741 commented on Jul 2, 2025 • 0 new comments

• Problem with `DISPLAY` pragma for `⊥` in `Data.Empty`

  #2493 commented on Jul 5, 2025 • 0 new comments

• Release of v2.3

  #2749 commented on Jul 6, 2025 • 0 new comments

• Replace record directive "eta-equality" by "no-eta-equality;pattern"

  #2476 commented on Jul 3, 2025 • 0 new comments