List view

[DRY] Refactor algebraic properties of types

breaking

dependencies

library-design

refactoring

Status: Closed (completed).

#2489 In agda/agda-stdlib;

· by jamesmckinna was closed on Feb 1, 2026

finer-grained analysis of NonZero arguments

breaking

refactoring

Status: Closed (abandoned).

agda/agda-stdlibnumber 2230

#2230 In agda/agda-stdlib;

· by jamesmckinna was closed on Dec 15, 2023

Implement ≤-total in terms of _≤?_

breaking

performance

refactoring

Status: Merged (completed).

agda/agda-stdlibnumber 2440

#2440 In agda/agda-stdlib;

· by Taneb was closed on Feb 8, 2025

[ refactor ] make contradiction and friends entirely definitionally proof-irrelevant

breaking

discussion

library-design

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: Closed (abandoned).

agda/agda-stdlibnumber 2802

#2802 In agda/agda-stdlib;

· by jamesmckinna was closed on Oct 30, 2025

Get rid of inconsistent ∙-cong name in algebra hierarchy?

breaking

discussion

naming

Status: Closed (completed).

#1544 In agda/agda-stdlib;

· by MatthewDaggitt was closed on Dec 9, 2024

Some properties of unnormalised rationals are named inconsistently

status: duplicateThe main contents of the issue or PR already exists in another issue or PR.The main contents of the issue or PR already exists in another issue or PR.

Status: Closed (completed).

#2550 In agda/agda-stdlib;

· by SlimTim10 was closed on Jan 15, 2025

Deprecate existing definition of ⊥-elim in favour of its irrelevant version ⊥-elim-irr

breaking

dependencies

deprecation

discussion

library-design

refactoring

Status: Closed (completed).

#2346 In agda/agda-stdlib;

· by jamesmckinna was closed on Dec 20, 2024

Unify general algebraic definitions of Divisibility and Primarity with those in Nat and Integer

library-design

status: duplicateThe main contents of the issue or PR already exists in another issue or PR.The main contents of the issue or PR already exists in another issue or PR.

Status: Closed (completed).

#2416 In agda/agda-stdlib;

· by mechvel was closed on Jul 11, 2024

[ fix ] parametrisation of Algebra.Consequences.Base

breaking

library-design

refactoring

status: duplicateThe main contents of the issue or PR already exists in another issue or PR.The main contents of the issue or PR already exists in another issue or PR.

Status: Closed (completed).

#2888 In agda/agda-stdlib;

· by jamesmckinna was closed on Nov 20, 2025

Pointed: Setoid with a distinguished point

addition

discussion

library-design

Status: Closed (completed).

#1957 In agda/agda-stdlib;

· by jamesmckinna was closed on Dec 20, 2024