Search code, repositories, users, issues, pull requests...

· 12/12

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

agda/agda-stdlib

#2797

· jamesmckinna opened

on Jul 31, 2025

· Changes requested

·

· 12/12

1

[ refactoring ] `Data.Fin.Properties.decFinSubset`

cosmetic

agda/agda-stdlib

#2793

· jamesmckinna opened

on Jul 30, 2025

· Changes requested

·

· 12/12

4

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

agda/agda-stdlib

#2790

· jamesmckinna opened

on Jul 28, 2025

· Review required

·

· 12/12

4

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

agda/agda-stdlib

#2787

· jamesmckinna opened

on Jul 27, 2025

· Approved

·

· 12/12

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

deprecation

#2786

· jamesmckinna opened

on Jul 27, 2025

·

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

#2770

· jamesmckinna opened

on Jul 15, 2025

1

4

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

agda/agda-stdlib

#2762

· jamesmckinna opened

on Jul 9, 2025

· Review required

·

hypothetical-rewrite

· 11/12

2

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

#2741

· jamesmckinna opened

on Jun 21, 2025

6

[ add ] lifting `{to|from}Witness` from `Relation.Nullary.Decidable.Core` to `Relation.Unary` and `Relation.Binary`

#2735

· jamesmckinna opened

on Jun 18, 2025

2

Cantor-Schröder-Bernstein, redux

#2728

· jamesmckinna opened

on Jun 5, 2025

9

A boolean algebra solver buried in `Algebra.Lattice.Properties.BooleanAlgebra.Expression`

#2702

· onestruggler opened

on Apr 15, 2025

8

[ refactor ] rationalise the common APIs for `List` and `Vec` versions of `Data..Relation.Binary.Lex.`

#2687

· jamesmckinna opened

on Mar 28, 2025

·

[ refactor ] Redefine `Relation.Binary.Definitions.Adjoint`, plus knock-on `Function.Consequences`

agda/agda-stdlib

#2599

· jamesmckinna opened

on Feb 19, 2025

· Review required

·

· 2/2

1

[ refactor ] use `variable`s in `Algebra.Consequences.Base`

agda/agda-stdlib

#2592

· jamesmckinna opened

on Feb 19, 2025

· Approved

·

· 2/2

9

[ refactor ] (Re)define `(Is)TightApartness` and `(Is)HeytingCommutativeRing`/`(Is)HeytingField`

agda/agda-stdlib

#2588

· jamesmckinna opened

on Feb 18, 2025

· Changes requested

·

· 2/2

19

[ refactor ] Symmetry of `Bijection` as a consequence of properties of a given `Surjective` function

agda/agda-stdlib

#2583

· jamesmckinna opened

on Feb 13, 2025

· Approved

·

· 2/2

6

Tidy up `Algebra.Definitions.RawMagma` (again), plus reconcile all the uses of `_,_` as a constructor

bug

#2582

· jamesmckinna opened

on Feb 12, 2025

4

[ refactor ] Reconcile `Relation.Binary.Definitions.Adjoint` and `Function.Definitions.Inverse*`

#2581

· jamesmckinna opened

on Feb 10, 2025

1

5

[ refactor ] Revise definitions, consequences, and use, of `Algebra.Definitions.(Almost)*Cancellative`

agda/agda-stdlib

#2573

· jamesmckinna opened

on Feb 6, 2025

· Approved

·

· 2/2

44

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

agda/agda-stdlib

#2572

· jamesmckinna opened

on Feb 6, 2025

· Approved

·

· 1/2

5

[ DRY ] Streamline `Function.*` hierarchy

deprecation

#2570

· jamesmckinna opened

on Jan 29, 2025

·

4

[ DRY ] Refactor `Function.*` to rationalise the existence of a section to a given `Surjective f`

#2568

· jamesmckinna opened

on Jan 28, 2025

·

1

[ refactor ] `Function.Definitions` and `Function.Consequences`?

#2565

· jamesmckinna opened

on Jan 28, 2025

7

[ refactor ] move `Data.List.Relation.Binary.Permutation.Setoid.Properties.foldr-commMonoid` to `Data.List.Effectful.Foldable`?

dependencies