List view

Ring reasoning

addition

Status: Draft (not ready).

agda/agda-stdlibnumber 2765

#2765 In agda/agda-stdlib;

· JacquesCarette opened on Jul 12, 2025

[ deprecate ] <code>Data.Fin.Base.lower₁</code> in favour of <code>Data.Fin.Base.lower</code>

deprecation

refactoring

Status: Open.

#2786 In agda/agda-stdlib;

· jamesmckinna opened on Jul 27, 2025

[ refactor ] <code>Data.Fin.Properties.decFinSubset</code>

cosmetic

refactoring

Status: Open (in progress).

agda/agda-stdlibnumber 2793

#2793 In agda/agda-stdlib;

· jamesmckinna opened on Jul 30, 2025

[ add ] clean version of <code>Data.Fin.Properties.searchMinimalCounterexample</code>

addition

refactoring

Status: Open (in progress).

agda/agda-stdlibnumber 2801

#2801 In agda/agda-stdlib;

· jamesmckinna opened on Aug 2, 2025

[ refactor ] reorganise <code>Relation.Nullary.Negation.Core</code> to make clean separation of properties

cosmetic

dependencies

refactoring

Status: Open (in progress).

agda/agda-stdlibnumber 2805

#2805 In agda/agda-stdlib;

· jamesmckinna opened on Aug 5, 2025

[ deprecate ] names for deMorgan lemmas in <code>Data.Fin.Properties</code>

deprecation

Status: Open (in progress).

agda/agda-stdlibnumber 2837

#2837 In agda/agda-stdlib;

· jamesmckinna opened on Oct 9, 2025

[ deprecate ] names for deMorgan lemmas in <code>Relation.Nullary.Negation</code>

deprecation

Status: Open (in progress).

agda/agda-stdlibnumber 2838

#2838 In agda/agda-stdlib;

· jamesmckinna opened on Oct 11, 2025