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

· 12/12

21

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

status: blocked-by-issue

agda/agda-stdlib

#2787

· jamesmckinna opened

on Jul 27, 2025

· Approved

·

· 12/12

2

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

agda/agda-stdlib

#2783

· jamesmckinna opened

on Jul 25, 2025

· Approved

·

· 12/12

14

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

#2741

· jamesmckinna opened

on Jun 21, 2025

6

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

#2687

· jamesmckinna opened

on Mar 28, 2025

·

Fragile `NonZero` and implementation-dependent luck

instances

#2644

· JacquesCarette opened

on Mar 5, 2025

·

Agda-future

11

Redefine `Algebra.Consequences.Setoid.wlog`

#2626

· jamesmckinna opened

on Feb 27, 2025

·

6

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

addition

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`

addition

agda/agda-stdlib

#2588

· jamesmckinna opened

on Feb 18, 2025

· Changes requested

·

· 2/2

19

[ refactor ] Definitions of `Relation.Binary.Apartness` and `Algebra..Heyting*`

#2587

· jamesmckinna opened

on Feb 18, 2025

·

[ 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

#2582

· jamesmckinna opened

on Feb 12, 2025

4

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

library-design

#2581

· jamesmckinna opened

on Feb 10, 2025

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 ] `Function.Definitions`, adding `Function.Definitions.Strict` module

agda/agda-stdlib

#2567

· jamesmckinna opened

on Jan 28, 2025

· Review required

· 2/2

[ refactor ] rectify binder names in `Relation.Binary.Definitions`

cosmetic

agda/agda-stdlib

#2552

· jamesmckinna opened

on Jan 15, 2025

· Approved

·

· 2/2

[ refactor ] Fix/rationalise 'legacy' binder names in `Relation.Binary.Definitions` (and elsewhere?)

library-design

#2547

· jamesmckinna opened

on Jan 14, 2025

·

1

Inconvenient precedences

library-design

#2531

· JacquesCarette opened

on Dec 20, 2024

8

[ refactor ] Exchange components of `Relation.Binary.Definitions._Respects₂_`

agda/agda-stdlib

#2515

· jamesmckinna opened

on Dec 9, 2024

· Changes requested

·

· 2/2

9

[DRY] Refactor algebraic properties of types

#2489

· jamesmckinna opened

on Oct 1, 2024

·

4

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

status: blocked-by-issue

upstream

agda/agda-stdlib

#2476

· andreasabel opened

on Sep 6, 2024

·

Agda-future

· 2/2

11

Find all single letter publicly-exported modules and make sure they are private

#2472

· MatthewDaggitt opened

on Sep 3, 2024

·