Search results

[ deprecate ] <code>Data.Fin.Permutation.Components</code>

deprecation

question

Status: Open.

#2752 In agda/agda-stdlib;

· jamesmckinna opened on Jun 26, 2025

 ·  

v2.4

Release of v2.3

release

Status: Open.

#2749 In agda/agda-stdlib;

· MatthewDaggitt opened on Jun 26, 2025

 ·  

v2.3

<code>IsString</code> typeclass isn't actually listed as an instance in <code>Data.List.Literals</code>

bug

Status: Open.

#2745 In agda/agda-stdlib;

· rvs314 opened on Jun 23, 2025

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

breaking

dependencies

deprecation

discussion

refactoring

Status: Open.

#2741 In agda/agda-stdlib;

· jamesmckinna opened on Jun 21, 2025

[ add ] lifting <code>{to|from}Witness</code> from <code>Relation.Nullary.Decidable.Core</code> to <code>Relation.Unary</code> and <code>Relation.Binary</code>

addition

refactoring

Status: Open.

#2735 In agda/agda-stdlib;

· jamesmckinna opened on Jun 18, 2025

Cantor-Schröder-Bernstein, redux

addition

refactoring

Status: Open.

#2728 In agda/agda-stdlib;

· jamesmckinna opened on Jun 5, 2025

<code>showHexa</code> from <code>Data.Word64.Show</code> blows up when normalizing from Emacs

Status: Open.

#2722 In agda/agda-stdlib;

· bkomuves opened on May 28, 2025

Add isMonotone Definition for Poset

Status: Open.

#2718 In agda/agda-stdlib;

· jmougeot opened on May 12, 2025

Clean up basic order theory definitions

Status: Open.

#2717 In agda/agda-stdlib;

· jmougeot opened on May 12, 2025

Problem with <code>Tactic.MonoidSolver</code>

Status: Open.

#2710 In agda/agda-stdlib;

· javierdiaz72 opened on Apr 30, 2025

Do we need a definition for <code>(Is)BooleanRing</code>?

Status: Open.

#2704 In agda/agda-stdlib;

· onestruggler opened on Apr 17, 2025

A boolean algebra solver buried in <code>Algebra.Lattice.Properties.BooleanAlgebra.Expression</code>

refactoring

Status: Open.

#2702 In agda/agda-stdlib;

· onestruggler opened on Apr 15, 2025