Search results

Proved sorted permutations are equal

addition

documentation

Status: Open (in progress).

agda/agda-stdlibnumber 2748

#2748 In agda/agda-stdlib;

· MatthewDaggitt opened on Jun 26, 2025

 ·  

v2.3

Lemmata for <code>if_then_else_</code>

addition

Status: Open (in progress).

agda/agda-stdlibnumber 2747

#2747 In agda/agda-stdlib;

· pmbittner opened on Jun 25, 2025

 ·  

v2.3

[ refactor ] (more) decidable <code>Data.Fin.Properties</code>

addition

cosmetic

refactoring

Status: Open (in progress).

agda/agda-stdlibnumber 2744

#2744 In agda/agda-stdlib;

· jamesmckinna opened on Jun 23, 2025

[ refactor ] <code>Data.Fin.Properties</code> of decidable equality, plus knock-ons

addition

dependencies

refactoring

Status: Open (in progress).

agda/agda-stdlibnumber 2740

#2740 In agda/agda-stdlib;

· jamesmckinna opened on Jun 21, 2025

 ·  

v2.3

[ add ] <code>Relation.Nullary.Decidable.dec-yes-recompute</code>

addition

deprecation

refactoring

Status: Open (in progress).

agda/agda-stdlibnumber 2738

#2738 In agda/agda-stdlib;

· jamesmckinna opened on Jun 20, 2025

 ·  

v2.3

Some extra support for homogeneous n-ary products

addition

deprecation

Status: Open (in progress).

agda/agda-stdlibnumber 2736

#2736 In agda/agda-stdlib;

· MatthewDaggitt opened on Jun 19, 2025

 ·  

v2.3

[ 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

Refactor <code>Data.Vec.Properties</code> : Add toList-injective and new lemmas

addition

Status: Open (in progress).

agda/agda-stdlibnumber 2733

#2733 In agda/agda-stdlib;

· jmougeot opened on Jun 9, 2025

 ·  

v2.3

Cantor-Schröder-Bernstein, redux

addition

refactoring

Status: Open.

#2728 In agda/agda-stdlib;

· jamesmckinna opened on Jun 5, 2025

[ add ] Choudhury and Fiore's alternative definition of <code>Permutation</code> for <code>Setoid</code>s

addition

refactoring

Status: Open (in progress).

agda/agda-stdlibnumber 2726

#2726 In agda/agda-stdlib;

· jamesmckinna opened on Jun 2, 2025

 ·  

v2.3

[Add] Initial files for Domain theory

addition

Status: Open (in progress).

agda/agda-stdlibnumber 2721

#2721 In agda/agda-stdlib;

· jmougeot opened on May 26, 2025

Adds Algebra.Morphism.Construct.DirectProduct

addition

Status: Open (in progress).

agda/agda-stdlibnumber 2715

#2715 In agda/agda-stdlib;

· carlostome opened on May 9, 2025

 ·  

v2.3