GitHub · Where software is built

Labels Milestones New issue

[ discussion ] alternative design for <code>Algebra.Structures.IsX</code> and <code>Algebra.Properties.X</code>

agda/agda-stdlib

#2762

· jamesmckinna opened

on Jul 9, 2025

·

hypothetical-rewrite

[ deprecate ] <code>Relation.Nullary.Reflects</code> and [ refactor ] <code>Relation.Nullary.Decidable.Core</code>

#2741

· jamesmckinna opened

on Jun 21, 2025

[ refactor ] <code>Data.Fin.Properties</code> of decidable equality, plus knock-ons

agda/agda-stdlib

#2740

· jamesmckinna opened

on Jun 21, 2025

·

[ refactor ] move <code>Data.List.Relation.Binary.Permutation.Setoid.Properties.foldr-commMonoid</code> to <code>Data.List.Effectful.Foldable</code>?

#2560

· jamesmckinna opened

on Jan 20, 2025

[ refactor ] Remove <code>sum</code> and <code>product</code> (and their properties) from <code>Data.List.*</code>

#2553

· jamesmckinna opened

on Jan 16, 2025

·

[ refactor ] Functoriality of <code>Data.List.Relation.Binary.Sublist|Subset</code> wrt <code>All</code> and <code>Any</code>

#2525

· jamesmckinna opened

on Dec 18, 2024

[DRY] Refactor algebraic properties of types

#2489

· jamesmckinna opened

on Oct 1, 2024

·

[DRY] Refactor the various definitions of 'pointwise' equality on functions/<code>Function</code>s/pointwise <code>Algebra</code>s

#2434

· jamesmckinna opened

on Jul 7, 2024

Rename <code>WeaklyDecidable</code>?

#2404

· jamesmckinna opened

on Jun 9, 2024

Refactor <code>Data.List.Relation.Binary.Permutation.*</code>

agda/agda-stdlib

#2317

· jamesmckinna opened

on Mar 12, 2024

Missing derived operations in <code>Algebra.Structures.IsGroup</code>/<code>Algebra.Bundles.Raw.RawGroup</code>

#2268

· jamesmckinna opened

on Jan 29, 2024

[DRY] Reconciling the indices of <code>IsX</code> with those of the corresponding <code>RawX</code>

#2252

· jamesmckinna opened

on Jan 11, 2024

·

hypothetical-rewrite