Issues

Issues

• [ add ] (yet) more Algebra.Properties.* re-exports: (yet) more diamonds

  agda/agda-stdlib#3139 · opened on Nov 10, 2026
  1

• More about Data.Rational.Properties

  agda/agda-stdlib#3136 · opened on Nov 6, 2026
  2

• [ add ] positive rationals ℚ⁺ as a type in their own right, with... suitable Properties

  agda/agda-stdlib#3134 · opened on Nov 3, 2026
  4

• takeWhile-accept and others

  agda/agda-stdlib#3130 · opened on Oct 25, 2026

• Needs lib-2.4 dropWhile⁺ in All ?

  agda/agda-stdlib#3121 · opened on Sep 22, 2026

• [ views ] 'smart(er) constructors', 'destructor form', ... how to describe/systematise this phenomenon?

  agda/agda-stdlib#3113 · opened on Sep 4, 2026

• New branch agda-master working with the master version of Agda

  agda/agda-stdlib#3112 · opened on Aug 29, 2026
  5

• [ Regex ] search with fromStart = true does not match as expect; request for documentation

  agda/agda-stdlib#3109 · opened on Aug 22, 2026

• [ fix ] Outstanding issues with existing Tactic.*Solver and Algebra.Solver.* implementations

  Task

  agda/agda-stdlib#3105 · opened on Aug 4, 2026 · v3.0

• [ refactor ] sort out the argument + constructor names in Relation.Binary.Closure.ReflexiveTransitive

  agda/agda-stdlib#3103 · opened on Aug 1, 2026
  1

• Items for SetoidMonomorphism

  agda/agda-stdlib#3096 · opened on Jul 30, 2026
  1

• [ add ] 'lax squares' in Relation.Binary and their horizontal/vertical compositions

  agda/agda-stdlib#3093 · opened on Jul 28, 2026
  4

• [ refactor ] rename + deprecate Data.List.Base. _∷ʳ′_

  agda/agda-stdlib#3089 · opened on Jul 26, 2026

• Add Queue datatype

  agda/agda-stdlib#3083 · opened on Jul 20, 2026

• map-cong for Setoid as a co-domain?

  agda/agda-stdlib#3082 · opened on Jul 20, 2026
  4

• Create abstraction barrier for _≤?_ from Data.Nat.Properties

  agda/agda-stdlib#3074 · opened on Jul 15, 2026
  2

• [ add ] Function.Metric.Core.DistanceRelation

  agda/agda-stdlib#3068 · opened on Jul 10, 2026

• [ refactor ] Renaming concepts in Relation.Binary.{Definitions|Structures|Bundles}

  agda/agda-stdlib#3058 · opened on Jul 8, 2026
  1

• [ question ] differences between Reasoning.Binary.Preorder and Reasoning.Binary.PartialOrder?

  agda/agda-stdlib#3047 · opened on Jul 2, 2026
  12

• Write a stdlib tutorial

  agda/agda-stdlib#3045 · opened on Jul 1, 2026

• [ add ] EverythingDEPRECATED?

  agda/agda-stdlib#3038 · opened on Jun 30, 2026
  4

• Add checks for defunct and orphaned READMEs to CI

  agda/agda-stdlib#3037 · opened on Jun 29, 2026
  2

• [ refactor ] Algebra.Morphism wrt re-exports from Algebra.Morphism.Definitions

  agda/agda-stdlib#3035 · opened on Jun 25, 2026
  4

• Deleting Function.Bijection and friends?

  agda/agda-stdlib#3033 · opened on Jun 24, 2026 · v3.0
  6

• Notes on lib-2.4 and a suggestion

  agda/agda-stdlib#3027 · opened on Jun 22, 2026