List view

Reimplement <code>Permutation.Propositional</code> in terms of <code>Permutation.Setoid</code>

breaking

refactoring

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.

#1354 In agda/agda-stdlib;

· MatthewDaggitt opened on Nov 11, 2020

Standardise record constructor names

breaking

documentation

naming

Status: Open.

#1388 In agda/agda-stdlib;

· mechvel opened on Dec 30, 2020

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

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

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

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

Preserve backwards compatibility across Agda versions

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.

#1877 In agda/agda-stdlib;

· turion opened on Nov 7, 2022

Deprecate <code>inspect</code> function in favour of new <code>with ... in</code> construct

deprecation

refactoring

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.

#1580 In agda/agda-stdlib;

· MatthewDaggitt opened on Aug 19, 2021

Simplify <code>Relation.Binary.Reasoning.Syntax</code> further

refactoring

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.

#2150 In agda/agda-stdlib;

· MatthewDaggitt opened on Oct 14, 2023