List view

Ring reasoning

addition

Status: Draft (not ready).

agda/agda-stdlibnumber 2765

#2765 In agda/agda-stdlib;

· JacquesCarette opened on Jul 12, 2025

[ add ] Algebra.Construct.Centre.X of an algebra X, following #2863

addition

Status: Open (in progress).

agda/agda-stdlibnumber 2885

#2885 In agda/agda-stdlib;

· jamesmckinna opened on Nov 19, 2025

[ deprecate ] README.Inspect

deprecation

documentation

Status: Open (in progress).

agda/agda-stdlibnumber 2928

#2928 In agda/agda-stdlib;

· jamesmckinna opened on Feb 4, 2026

[ refactor ] make Relation.Binary.Morphism.Definitions obsolete

dependencies

library-design

Status: Open (in progress).

agda/agda-stdlibnumber 2922

#2922 In agda/agda-stdlib;

· jamesmckinna opened on Jan 24, 2026

[ refactor ] name of Data.Product.Relation.Binary.Pointwise.NonDependent.×-decidable

deprecation

refactoring

Status: Open (in progress).

agda/agda-stdlibnumber 2958

#2958 In agda/agda-stdlib;

· jamesmckinna opened on Mar 2, 2026

[ refactor ] introduce revised notation for decidability of Lexicographic orderings, plus knock-ons

deprecation

refactoring

Status: Open (in progress).

agda/agda-stdlibnumber 2963

#2963 In agda/agda-stdlib;

· jamesmckinna opened on Mar 9, 2026

[ refactor ] Infrastructure for Data.Tree.AVL.Indexed.*

addition

cosmetic

dependencies

refactoring

Status: Open (in progress).

agda/agda-stdlibnumber 2968

#2968 In agda/agda-stdlib;

· jamesmckinna opened on Mar 20, 2026

[ refactor ] downstream improvements following #2961 / #2968

refactoring

status: blocked-by-issueProgress on this issue or PR is blocked by another issue.Progress on this issue or PR is blocked by another issue.

Status: Draft (not ready).

agda/agda-stdlibnumber 2970

#2970 In agda/agda-stdlib;

· jamesmckinna opened on Mar 25, 2026

[ add ] injectivity of suc for relation m ≡ n (mod o) for {{NonZero o}}

addition

Status: Open (in progress).

agda/agda-stdlibnumber 2971

#2971 In agda/agda-stdlib;

· jamesmckinna opened on Mar 27, 2026

[ fix ] #2865 for the remaining Data.*.Relation.Unary.Any

deprecation

naming

Status: Open (in progress).

agda/agda-stdlibnumber 2972

#2972 In agda/agda-stdlib;

· jamesmckinna opened on Apr 1, 2026