Skip to content

Pull requests: agda/agda-stdlib

New pull request New
60 Open 1,726 Closed
60 Open 1,726 Closed
Author
Filter by author
Loading
Label
Filter by label
Loading
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Projects
Filter by project
Loading
Milestones
Filter by milestone
Loading
Reviews
Filter by reviews
No reviews Review required Approved review Changes requested
Assignee
Filter by who’s assigned
Assigned to nobody Loading
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Pull requests list

[ fix ] assumption name in Data.Product.Relation.Binary.Lex.Strict cosmetic
#2956 opened Feb 27, 2026 by jamesmckinna Loading…
[ rename ] decidability for Relation.Binary.Construct.{Intersection|Union}` cosmetic deprecation low-hanging-fruit status: blocked-by-issue Progress on this issue or PR is blocked by another issue.
#2955 opened Feb 27, 2026 by jamesmckinna Loading…
1
[ refactor ] fix #2865
#2954 opened Feb 25, 2026 by jamesmckinna Loading… v2.4
2
[Add] Properties of rounding in Rational
#2953 opened Feb 25, 2026 by aortega0703 • Draft
24
[ breaking ] change fieldname _≟_ to _≈?_ in IsDecEquivalence breaking deprecation library-design refactoring style-guide
#2952 opened Feb 25, 2026 by jamesmckinna Loading… v2.4
1
11
[ deprecate ] Relation/Binary.PropositionalEquality.inspect (#1580 / #1630 / #1930 redux) deprecation library-design status: blocked-by-issue Progress on this issue or PR is blocked by another issue.
#2934 opened Feb 6, 2026 by jamesmckinna Loading…
1
3
[ deprecate ] README.Inspect deprecation documentation
#2928 opened Feb 4, 2026 by jamesmckinna Loading… v2.4
3
[ add ] Nat lemmas with _∸_, _⊔_ and _⊓_ addition
#2924 opened Jan 26, 2026 by jkopanski Loading… v2.4
24
[ refactor ] make Relation.Binary.Morphism.Definitions obsolete dependencies library-design
#2922 opened Jan 24, 2026 by jamesmckinna Loading… v2.4
11
[ refactor ] use variables more systematically in Data.List.Fresh{.*} cosmetic discussion library-design refactoring
#2916 opened Jan 23, 2026 by jamesmckinna Loading… v2.4
17
[ add ] left- and right- actions induced by a Magma homomorphism addition library-design
#2894 opened Nov 24, 2025 by jamesmckinna • Draft
9
Attempt at the INT construction
#2891 opened Nov 23, 2025 by Taneb • Draft
1
22
[ add ] Algebra.Construct.Centre.X of an algebra X, following #2863 addition
#2885 opened Nov 19, 2025 by jamesmckinna Loading… v2.4
10
[ draft ] Alternative design for sub- and quotient- (Abelian)Groups addition library-design refactoring
#2859 opened Nov 5, 2025 by jamesmckinna • Draft
30
Add principal ideal construction
#2857 opened Nov 3, 2025 by Taneb • Draft
8
Add ideals and quotient rings
#2855 opened Oct 31, 2025 by Taneb • Draft
30
Normal subgroups and quotient groups
#2854 opened Oct 31, 2025 by Taneb Loading…
41
[ add ] Data.Bool.contradiction fixing #2847 addition
#2853 opened Oct 30, 2025 by jamesmckinna • Draft
2
Algebra property reexports
#2851 opened Oct 29, 2025 by Taneb Loading…
18
Filters - alternative to the base of Domain theory
#2829 opened Sep 11, 2025 by gabriellisboaconegero Loading…
3
Add formalization of substructural logics in src
#2825 opened Sep 4, 2025 by mlebar-UC Loading…
35
Add cartesianProductWith⁻ and cartesianProduct⁻ to All
#2824 opened Sep 3, 2025 by javierdiaz72 Loading…
8
[ add ] PartialOrder structure/bundle on _→_ (fixes issue #2820) addition
#2823 opened Aug 31, 2025 by jamesmckinna Loading…
1
1
[draft] Polynomial
#2821 opened Aug 29, 2025 by samparkky • Draft
26
[ add ] Pointwise lifting of algebra to Data.Vec.Functional (Functional vector module #1945 redux)
#2817 opened Aug 28, 2025 by e-mniang Loading…
@JacquesCarette
45
ProTip! Add no:assignee to see everything that’s not assigned.