v3.0

New issue

Open

No due date

•Last updated Aug 5, 2026

59% complete

Add type classes and .Instance modules declaring their instances
agda/agda-stdlib#1332 · opened on Oct 23, 2020 · v3.0
6
Increasing the amount of re-exporting in Data.X
agda/agda-stdlib#619 · opened on Feb 15, 2019 · v3.0
6
Use instance fields for superclasses (?)
agda/agda-stdlib#1529 · opened on Jun 27, 2021 · v3.0
5
Add structures/bundles for pairs of strict and non-strict orders
agda/agda-stdlib#1179 · opened on Apr 29, 2020 · v3.0
4
There should be level-polymorphic versions of the combinators in Data.List.Categorical
agda/agda-stdlib#951 · opened on Oct 18, 2019 · v3.0
8
generic Nonzero proposal
agda/agda-stdlib#1175 · opened on Apr 28, 2020 · v3.0
19
names of things (vol. 94): Relation.Nullary.Reflects
agda/agda-stdlib#2058 · opened on Aug 15, 2023 · v3.0
Reconciling Data.Nat.Divisibility.Core._∣_ and Algebra.Definitions.RawMagma._∣_
agda/agda-stdlib#2115 · opened on Sep 29, 2023 · v3.0
17
Consider where we can use opaque mechanism to provide abstraction
agda/agda-stdlib#2136 · opened on Oct 12, 2023 · v3.0
5
Standardisation of folds
agda/agda-stdlib#278 · opened on Apr 13, 2018 · v3.0
21
Misnomer: Relation.Binary.Definitions.Total
agda/agda-stdlib#453 · opened on Sep 5, 2018 · v3.0
11
AlmostCancellative in Nat.Properties ?
agda/agda-stdlib#1562 · opened on Jul 26, 2021 · v3.0
3
Inconsistent naming between Data.(Nat/Integer).Properties
agda/agda-stdlib#1579 · opened on Aug 12, 2021 · v3.0
10
Should StrictTotalOrder be decidable?
agda/agda-stdlib#452 · opened on Sep 5, 2018 · v3.0
15
List of wrinkles in Data.List.Properties
agda/agda-stdlib#2358 · opened on Apr 11, 2024 · v3.0
8
Splitting Data.Char.Base
agda/agda-stdlib#1489 · opened on Apr 25, 2021 · v3.0
7
Vec.Properties: drop eq parameter when it is a property (v3.0 changes)
Unread
#2431 opened Jul 5, 2024 · Updated Jul 11, 2026Draft
5
Unsolved metas in Data.List.Properties cf. discussion on #2415, #2359, #2365
agda/agda-stdlib#2427 · opened on Jul 4, 2024 · v3.0
5
Rename Data.List.Properties.*-is-foldr
agda/agda-stdlib#2516 · opened on Dec 11, 2024 · v3.0
1
Flipped type signatures in comments
agda/agda-stdlib#1825 · opened on Sep 18, 2022 · v3.0
7
[ refactor ] Reconcile left/right congruence statements and proofs
agda/agda-stdlib#2532 · opened on Dec 22, 2024 · v3.0
12
[ refactor ] Remove sum and product (and their properties) from Data.List.*
agda/agda-stdlib#2553 · opened on Jan 16, 2025 · v3.0
7
[ refactor ] Definitions of Relation.Binary.Apartness and Algebra.*.*Heyting*
agda/agda-stdlib#2587 · opened on Feb 18, 2025 · v3.0
[ refactor ] (Re)define (Is)TightApartness and (Is)HeytingCommutativeRing/(Is)HeytingField
Unread
#2588 opened Feb 18, 2025 · Updated Jul 21, 2026
32
[ refactor ] rationalise the common APIs for List and Vec versions of Data.*.Relation.Binary.Lex.*
agda/agda-stdlib#2687 · opened on Mar 28, 2025 · v3.0

Navigation Menu

v3.0

Add type classes and `.Instance` modules declaring their instances

Increasing the amount of re-exporting in `Data.X`

Use instance fields for superclasses (?)

Add structures/bundles for pairs of strict and non-strict orders

There should be level-polymorphic versions of the combinators in `Data.List.Categorical`

generic Nonzero proposal

names of things (vol. 94): `Relation.Nullary.Reflects`

Reconciling `Data.Nat.Divisibility.Core._∣_` and `Algebra.Definitions.RawMagma._∣_`

Consider where we can use `opaque` mechanism to provide abstraction

Standardisation of folds

Misnomer: `Relation.Binary.Definitions.Total`

AlmostCancellative in Nat.Properties ?

Inconsistent naming between `Data.(Nat/Integer).Properties`

Should StrictTotalOrder be decidable?

List of wrinkles in `Data.List.Properties`

Splitting `Data.Char.Base`

Vec.Properties: drop eq parameter when it is a property (v3.0 changes)

Unsolved metas in `Data.List.Properties` cf. discussion on #2415, #2359, #2365

Rename `Data.List.Properties.*-is-foldr`

Flipped type signatures in comments

[ refactor ] Reconcile left/right congruence statements and proofs

[ refactor ] Remove `sum` and `product` (and their properties) from `Data.List.*`

[ refactor ] Definitions of `Relation.Binary.Apartness` and `Algebra..Heyting*`

[ refactor ] (Re)define `(Is)TightApartness` and `(Is)HeytingCommutativeRing`/`(Is)HeytingField`

[ refactor ] rationalise the common APIs for `List` and `Vec` versions of `Data..Relation.Binary.Lex.`

Issues