Search results

[ DRY ] Streamline <code>Function.*</code> hierarchy

deprecation

library-design

refactoring

Status: Open.

#2570 In agda/agda-stdlib;

· jamesmckinna opened on Jan 29, 2025

 ·  

v3.0

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

dependencies

deprecation

library-design

refactoring

Status: Open.

#2553 In agda/agda-stdlib;

· jamesmckinna opened on Jan 16, 2025

 ·  

v3.0

Rename <code>Data.List.Properties.*-is-foldr</code>

bikeshedding

cosmetic

deprecation

library-design

naming

refactoring

Status: Open.

#2516 In agda/agda-stdlib;

· jamesmckinna opened on Dec 11, 2024

 ·  

v3.0

Reconciling <code>Data.Nat.Divisibility.Core._∣_</code> and <code>Algebra.Definitions.RawMagma._∣_</code>

breaking

deprecation

discussion

library-design

refactoring

Status: Open.

#2115 In agda/agda-stdlib;

· jamesmckinna opened on Sep 29, 2023

 ·  

v3.0

names of things (vol. 94): <code>Relation.Nullary.Reflects</code>

cosmetic

deprecation

library-design

naming

Status: Open.

#2058 In agda/agda-stdlib;

· jamesmckinna opened on Aug 15, 2023

 ·  

v3.0

Deprecate <code>inspect</code> function in favour of new <code>with ... in</code> construct

deprecation

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.

upstreamChanges induced by Agda upstreamChanges induced by Agda upstream

Status: Open.

#1580 In agda/agda-stdlib;

· MatthewDaggitt opened on Aug 19, 2021

 ·  

Agda-future

Bracket more consistently in names

deprecation

naming

refactoring

Status: Open.

#1130 In agda/agda-stdlib;

· mechvel opened on Mar 28, 2020

Have a systematic way of marking a module as 'experimental'

deprecation

discussion

Status: Open.

#1124 In agda/agda-stdlib;

· gallais opened on Mar 22, 2020

Deprecate <code>Algebra.Solver.Ring</code> in favour of <code>Tactic.RingSolver</code>

deprecation

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.

tactics

Status: Open.

#1069 In agda/agda-stdlib;

· MatthewDaggitt opened on Jan 25, 2020