Search results

Maybe avoid introducing almost undefined arguments?

Status: Open.

#2772 In agda/agda-stdlib;

· mechvel opened on Jul 15, 2025

[ refactor ] change type of <code>Data.Vec.Base.{truncate|padRight}</code>

refactoring

Status: Open.

#2770 In agda/agda-stdlib;

· jamesmckinna opened on Jul 15, 2025

[ add ] <code>Level</code>-lifting for <code>Relation.Binary.{Structures|Bundles}</code> and <code>Algebra.{Structures|Bundles}</code>

Status: Open.

#2767 In agda/agda-stdlib;

· jamesmckinna opened on Jul 13, 2025

Setoid for List composed n-times: second level is constrained to &gt;= first level

Status: Open.

#2766 In agda/agda-stdlib;

· mechvel opened on Jul 11, 2025

[ definition ] characteristic of a <code>Ring</code> (etc.)

addition

library-design

question

Status: Open.

#2760 In agda/agda-stdlib;

· jamesmckinna opened on Jul 7, 2025

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