Search results

[ 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

 ·  

v2.3

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

infixity mismatch between <code>_∧_</code> and the ring multiplication <code>_*_</code>

bug

Status: Open.

#2701 In agda/agda-stdlib;

· onestruggler opened on Apr 15, 2025

 ·  

v3.0

Algebra.Solver.Ring allows us to specify a coefficient ring, but not here

bug

Status: Open.

#2700 In agda/agda-stdlib;

· onestruggler opened on Apr 14, 2025

Missing <code>padRight</code> properties

addition

low-hanging-fruit

Status: Open.

Feature

#2696 In agda/agda-stdlib;

· gallais opened on Apr 11, 2025

Implementation of consequences and lemmas for Groups

Status: Open.

#2695 In agda/agda-stdlib;

· jmougeot opened on Apr 11, 2025