Issues

• Needs lib-2.4 dropWhile⁺ in All ?

  agda/agda-stdlib#3121 · Filter by author mechvel opened on Sep 22, 2026

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

  agda/agda-stdlib#3113 · Filter by author jamesmckinna opened on Sep 4, 2026

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

  upstream
  agda/agda-stdlib#3112 · Filter by author andreasabel opened on Aug 29, 2026
  4

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

  agda/agda-stdlib#3109 · Filter by author joha2 opened on Aug 22, 2026

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

  Task

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

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

  namingrefactoring
  agda/agda-stdlib#3103 · Filter by author jamesmckinna opened on Aug 1, 2026
  1

• Items for SetoidMonomorphism

  agda/agda-stdlib#3096 · Filter by author mechvel opened on Jul 30, 2026
  1

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

  agda/agda-stdlib#3093 · Filter by author jamesmckinna opened on Jul 28, 2026
  4

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

  deprecationlibrary-designnamingrefactoring
  agda/agda-stdlib#3089 · Filter by author jamesmckinna opened on Jul 26, 2026

• Add Queue datatype

  agda/agda-stdlib#3083 · Filter by author silas-hw opened on Jul 20, 2026

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

  agda/agda-stdlib#3082 · Filter by author mechvel opened on Jul 20, 2026
  4

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

  agda/agda-stdlib#3074 · Filter by author JacquesCarette opened on Jul 15, 2026
  2

• [ add ] Function.Metric.Core.DistanceRelation

  agda/agda-stdlib#3068 · Filter by author jamesmckinna opened on Jul 10, 2026

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

  breakingrefactoring
  agda/agda-stdlib#3058 · Filter by author jamesmckinna opened on Jul 8, 2026
  1

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

  agda/agda-stdlib#3047 · Filter by author jamesmckinna opened on Jul 2, 2026
  12

• Write a stdlib tutorial

  agda/agda-stdlib#3045 · Filter by author JacquesCarette opened on Jul 1, 2026

• [ add ] EverythingDEPRECATED?

  agda/agda-stdlib#3038 · Filter by author jamesmckinna opened on Jun 30, 2026
  4

• Add checks for defunct and orphaned READMEs to CI

  agda/agda-stdlib#3037 · Filter by author silas-hw opened on Jun 29, 2026
  2

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

  agda/agda-stdlib#3035 · Filter by author jamesmckinna opened on Jun 25, 2026
  4

• Deleting Function.Bijection and friends?

  deprecationlibrary-designlow-hanging-fruitrefactoring
  agda/agda-stdlib#3033 · Filter by author JacquesCarette opened on Jun 24, 2026 · v3.0
  6

• Notes on lib-2.4 and a suggestion

  agda/agda-stdlib#3027 · Filter by author mechvel opened on Jun 22, 2026

• [ add ] improve/refactor proofs of Data.Bool.ListAction.Properties

  additionrefactoring
  agda/agda-stdlib#3016 · Filter by author jamesmckinna opened on Jun 17, 2026

• Ring homomorphism from the integers to the rationals

  additionstatus: info needed
  agda/agda-stdlib#3006 · Filter by author andreasabel opened on Jun 9, 2026
  5

• Remove Algebra.Module.Morphism.ModuleHomomorphism

  agda/agda-stdlib#2995 · Filter by author Taneb opened on May 6, 2026

• Algebra.Morphism.SemiringMonomorphism

  agda/agda-stdlib#2988 · Filter by author mechvel opened on Apr 28, 2026
  3