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

agda/agda-stdlib

#2776

· jamesmckinna opened

on Jul 18, 2025

·

v2.3

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

#2701

· onestruggler opened

on Apr 15, 2025

·

Algebra.Solver.Ring allows us to specify a coefficient ring, but not here

#2700

· onestruggler opened

on Apr 14, 2025

Fragile `NonZero` and implementation-dependent luck

instances

#2644

· JacquesCarette opened

on Mar 5, 2025

·

Agda-future

Redefine `Algebra.Consequences.Setoid.wlog`

#2626

· jamesmckinna opened

on Feb 27, 2025

·

[ 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

·

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

#2582

· jamesmckinna opened

on Feb 12, 2025

Inconvenient precedences

library-design

#2531

· JacquesCarette opened

on Dec 20, 2024

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

agda/agda-stdlib

#2515

· jamesmckinna opened

on Dec 9, 2024

·

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

#2472

· MatthewDaggitt opened

on Sep 3, 2024

·

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

#2471

· jamesmckinna opened

on Sep 2, 2024

·

Unsolved metas in `Data.List.Properties` cf. discussion on #2415, #2359, #2365

#2427

· jamesmckinna opened

on Jul 4, 2024

·

Fix #2396 by removing redundant zero in IsNonAssociativeRing

agda/agda-stdlib

#2410

· lexvanderstoep opened

on Jun 16, 2024

·

[DRY] More redundant `zero` fields in `Algebra.Structures`

addition

#2396

· jamesmckinna opened

on May 27, 2024

Consistently add the equality after `resp` in proof names.

naming

#2341

· mechvel opened

on Apr 2, 2024

Parsing problems with the `PermutationReasoning` combinators in `Data.List.Relation.Binary.Permutation.Propositional`

#2319

· jamesmckinna opened

on Mar 14, 2024

Missing reexports in function bundles

#2229

· Taneb opened

on Dec 13, 2023

CI never sets AGDA_COMMIT in certain runs

continuous-integration

#2188

· andreasabel opened

on Oct 31, 2023

Relations in proofs in `Data.Product.Relation.Binary.Pointwise.NonDependent` don't appear to be inferable

#2174

· MatthewDaggitt opened

on Oct 20, 2023

Dependencies of `Reflection.AST.Argument.Information`

dependencies

#1864

· MatthewDaggitt opened

on Oct 25, 2022

Flipped type signatures in comments

documentation

#1825

· MatthiasHu opened

on Sep 18, 2022

·

Inconsistent naming between `Data.(Nat/Integer).Properties`

naming

#1579

· MatthewDaggitt opened

on Aug 12, 2021

·

Fix the mentions of defunct `README` modules

continuous-integration

documentation

low-hanging-fruit

#1380

· gallais opened

on Dec 14, 2020

Strict inequality on Float is unintuitive