1 Release published by 1 person

• v2.3

  published Aug 2, 2025

15 Pull requests merged by 5 people

• [ add ] style-guide recommendation preferring contradiction over ⊥-elim

  #2798 merged Aug 6, 2025

• [Add] padRight properties to Data.Vec.Properties

  #2769 merged Aug 5, 2025

• [ add ] eta law for ¬¬ monad

  #2803 merged Aug 5, 2025

• Backport changes from 2.3 release to 2.4

  #2799 merged Aug 2, 2025

• [ fix ] release guide

  #2800 merged Aug 2, 2025

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

  #2740 merged Aug 2, 2025

• [ refactor ] weaken type of Relation.Nullary.Negation.Core.contradiction-irr

  #2785 merged Aug 2, 2025

• Issue2788

  #2794 merged Aug 2, 2025

• [ add ] commentary explaining the IsXRing design problem (issues #1617 and #2771)

  #2781 merged Jul 31, 2025

• [ add ] rule of signs for RingWithoutOne

  #2761 merged Jul 31, 2025

• [ DRY ] redefine Algebra.Definitions.Medial in terms of Interchangable

  #2764 merged Jul 31, 2025

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

  #2726 merged Jul 31, 2025

• [ refactor ] CHANGELOG for v2.3-rc2

  #2776 merged Jul 31, 2025

• [ add ] ∸-suc lemma for natural numbers

  #2757 merged Jul 28, 2025

• [ fix ] type error in README.Data.Fin.Relation.Unary.Top

  #2791 merged Jul 28, 2025

16 Pull requests opened by 4 people

• [ refactor ] `Data.Fin.Properties` following #2746

  #2782 opened Jul 25, 2025

• [ refactor ] make `n≢i : n ≢ toℕ i` argument to `lower₁` irrelevant

  #2783 opened Jul 25, 2025

• [ refactor ] make `m ≤ n` argument to `Data.Vec.Base.{truncate|padRight}` irrelevant

  #2787 opened Jul 27, 2025

• [ refactor ] make `i ≢ j` argument to `Data.Fin.Base.punchOut` irrelevant

  #2790 opened Jul 28, 2025

• [ refactor ] `Data.Fin.Properties.decFinSubset`

  #2793 opened Jul 30, 2025

• [Add] truncate properties to Data.Vec.Properties

  #2795 opened Jul 30, 2025

• [add] partial elements in Effect.Monad.Partial module

  #2796 opened Jul 30, 2025

• [ add ] flipped version of `Relation.Nullary.Negation.Core.contradiction`

  #2797 opened Jul 31, 2025

• [ add ] clean version of `Data.Fin.Properties.searchMinimalCounterexample`

  #2801 opened Aug 2, 2025

• [ refactor ] make `contradiction` and friends entirely definitionally proof-irrelevant

  #2802 opened Aug 4, 2025

• [ refactor ] reorganise `Relation.Nullary.Negation.Core` to make clean separation of properties

  #2805 opened Aug 5, 2025

• [ refactor ] `Data.List.Relation.Binary.Sublist.Propositional.Properties`

  #2808 opened Aug 13, 2025

• [Add] Initial files for Domain theory - Continuation of #2721

  #2809 opened Aug 13, 2025

• Module morphisms polymorphic in the underlying ring structure

  #2810 opened Aug 15, 2025

• Predomains

  #2811 opened Aug 20, 2025

• [ add ] `Pointed` extension of an ordering

  #2813 opened Aug 20, 2025

7 Issues closed by 2 people

• [Add] takeNat for Vec in Data.Vec.Base

  #2778 closed Aug 16, 2025

• There should a lemma says Bijective implies Inverse^b in Function.Consequences

  #2806 closed Aug 16, 2025

• Prefer `contradiction` over `⊥-elim` when it makes sense?

  #2653 closed Aug 6, 2025

• 2.3-rc1 calls itself 2.2?

  #2779 closed Aug 2, 2025

• Release of v2.3

  #2749 closed Aug 2, 2025

• [ bug ] missing commits from v2.0 onwards

  #2788 closed Aug 2, 2025

• Refactor to support multiple definitions of `Data.List.Relation.Binary.Permutation`

  #2311 closed Jul 31, 2025

6 Issues opened by 2 people

• `Monotonicity` implies `Congruence` for `Antisymmetric` orderings

  #2812 opened Aug 20, 2025

• Orientation of the equation `Algebra.Properties.RingWithoutOne.-‿distribˡ-*`

  #2807 opened Aug 12, 2025

• [ design ] Re-exports from `Algebra.Properties.X`

  #2804 opened Aug 4, 2025

• Why we should revert stdlib to `--without-K` instead of using `--cubical-compatible`

  #2792 opened Jul 29, 2025

• [ deprecate ] `Data.Fin.Base.lower₁` in favour of `Data.Fin.Base.lower`

  #2786 opened Jul 27, 2025

• [ add ] new name for `flip`ped version of `Relation.Nullary.Negation.Core.contradiction`

  #2784 opened Jul 26, 2025

24 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.

• Modular arithmetic in terms of ideals

  #2729 commented on Aug 19, 2025 • 29 new comments

• [Add] Properties for DCPOs in `Relation.Binary.Properties.Domain`

  #2734 commented on Aug 2, 2025 • 13 new comments

• [Add] Initial files for Domain theory

  #2721 commented on Aug 18, 2025 • 3 new comments

• [ new ] Effect.Monad.Random

  #2372 commented on Aug 1, 2025 • 3 new comments

• [ add ] `Algebra.Definitions.Integral` and its consequences

  #2563 commented on Jul 31, 2025 • 1 new comment

• Ring reasoning

  #2765 commented on Jul 23, 2025 • 0 new comments

• [ add ] `BooleanRing` plus `Properties`

  #2763 commented on Aug 19, 2025 • 0 new comments

• [ discussion ] alternative design for `Algebra.Structures.IsX` and `Algebra.Properties.X`

  #2762 commented on Jul 23, 2025 • 0 new comments

• [ refactor ] Add equality as a parameter to `Algebra.Consequences.Base`

  #2572 commented on Jul 31, 2025 • 0 new comments

• Refactor `Algebra.Solver.*Monoid` (further!)

  #2457 commented on Aug 2, 2025 • 0 new comments

• Add new `Bool` action on a `RawMonoid` plus properties

  #2450 commented on Jul 31, 2025 • 0 new comments

• Add `Algebra.Action.*` and friends

  #2350 commented on Jul 31, 2025 • 0 new comments

• Refactor `Data.List.Relation.Binary.Permutation.*`

  #2317 commented on Jul 31, 2025 • 0 new comments

• Add new module `Effect.Functor.Naperian`

  #2004 commented on Jul 31, 2025 • 0 new comments

• The free `Magma` on a `Set`, resp. `Setoid` [bis]

  #1962 commented on Aug 1, 2025 • 0 new comments

• [ fix #1354 ] Refactoring Permutation.Propositional

  #1761 commented on Aug 5, 2025 • 0 new comments

• Orders without equivalence relations

  #2070 commented on Aug 18, 2025 • 0 new comments

• [ refactor ] Functoriality of `Data.List.Relation.Binary.Sublist|Subset` wrt `All` and `Any`

  #2525 commented on Aug 13, 2025 • 0 new comments

• Substructures and quotients in the `Algebra.*` hierarchy

  #1899 commented on Aug 8, 2025 • 0 new comments

• [ refactor ] change type of `Data.Vec.Base.{truncate|padRight}`

  #2770 commented on Aug 5, 2025 • 0 new comments

• Implementation of consequences and lemmas for Groups

  #2695 commented on Aug 4, 2025 • 0 new comments

• infixity mismatch between `_∧_` and the ring multiplication `_*_`

  #2701 commented on Aug 1, 2025 • 0 new comments

• In CommutativeRing, Ring.semiring ≠ CommutativeSemiring.semiring

  #898 commented on Jul 23, 2025 • 0 new comments

• Do we need a definition for `(Is)BooleanRing`?

  #2704 commented on Jul 23, 2025 • 0 new comments