Search results

Redundant uses of <code>with</code>

discussion

library-design

Status: Open.

#1937 In agda/agda-stdlib;

· jamesmckinna opened on Mar 19, 2023

Substructures and quotients in the <code>Algebra.*</code> hierarchy

addition

discussion

library-design

Status: Open.

#1899 In agda/agda-stdlib;

· jamesmckinna opened on Jan 3, 2023

Split <code>Equality</code> and <code>Order</code> out of <code>Relation.Binary</code>

discussion

library-design

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.

#1763 In agda/agda-stdlib;

· MatthewDaggitt opened on May 4, 2022

 ·  

Agda-future

Operations on List's <code>All</code> defined in <code>Properties</code>

discussion

library-design

Status: Open.

#1583 In agda/agda-stdlib;

· ajrouvoet opened on Aug 26, 2021

Explore further improving instance search for <code>NonZero</code> instances

addition

discussion

instances

library-design

upstreamChanges induced by Agda upstreamChanges induced by Agda upstream

Status: Open.

#1565 In agda/agda-stdlib;

· MatthewDaggitt opened on Jul 29, 2021

 ·  

Agda-future

Use instance fields for superclasses (?)

discussion

instances

Status: Open.

#1529 In agda/agda-stdlib;

· jespercockx opened on Jun 27, 2021

 ·  

v3.0

Should the index argument <code>I</code> be implicit or explicit for indexed relations?

breaking

discussion

Status: Open.

#1519 In agda/agda-stdlib;

· MatthewDaggitt opened on Jun 13, 2021

 ·  

Agda-future

Splitting <code>Data.Char.Base</code>

discussion

library-design

Status: Open.

#1489 In agda/agda-stdlib;

· JacquesCarette opened on Apr 25, 2021

 ·  

v3.0

Refactoring <code>StrictToNonStrict</code> and <code>Closure.Reflexive</code>?

breaking

discussion

refactoring

upstreamChanges induced by Agda upstreamChanges induced by Agda upstream

Status: Open.

#1344 In agda/agda-stdlib;

· gallais opened on Nov 3, 2020

 ·  

Agda-future

Systematic support for checked and synthesised levels

discussion

library-design

Status: Open.

#1339 In agda/agda-stdlib;

· laMudri opened on Oct 29, 2020

Strict inequality on Float is unintuitive

breaking

bug

discussion

Status: Open.

#1284 In agda/agda-stdlib;

· wenkokke opened on Aug 25, 2020

Naming of unfolding lemmas

discussion

naming

Status: Open.

#1252 In agda/agda-stdlib;

· gallais opened on Jul 6, 2020