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

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

·

1

[ 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

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 ] `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

·

5

`Relation.Binary.Definitions._Respects₂_` seems to exchange 'left' and 'right' in its left/right projections?

#2471

· jamesmckinna opened

on Sep 2, 2024

·

1

3

Rename `homo` to `∙-homo` in `Algebra.Morphism.Structures`

agda/agda-stdlib

#2464

· jamesmckinna opened

on Aug 29, 2024

· Approved

·

· 2/2

14

Get rid of inconsistent `homo` name in algebra hierarchy?

discussion

naming

#2458

· jamesmckinna opened

on Aug 15, 2024

1

5

Vec.Properties: drop eq parameter when it is a property (v3.0 changes)

agda/agda-stdlib

#2431

· mildsunrise opened

on Jul 5, 2024

· Review required

·

· 2/2

Fix #2396 by removing redundant zero in IsNonAssociativeRing

agda/agda-stdlib

#2410

· lexvanderstoep opened

on Jun 16, 2024

· Approved

·