Skip to content

Pull requests: agda/agda-stdlib

New pull request New
53 Open 1,818 Closed
53 Open 1,818 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

[ add ] Data.Vec.Recursive.Relation.Binary.Pointwise
#3110 opened Aug 27, 2026 by jkopanski Contributor Loading…
Another Prop experiment
#3108 opened Aug 11, 2026 by Taneb Member • Draft
1
Add negatives for commutative monoids and semirings (Abelian group and ring completions)
#3106 opened Aug 5, 2026 by LionOfJewdah Loading…
16
[ add ] more text about negation and deduction from it (fixes #3099) style-guide
#3100 opened Jul 31, 2026 by jamesmckinna Collaborator Loading…
1
1
Add Show class
#3098 opened Jul 30, 2026 by silas-hw Contributor • Draft
1
24
[ refactor ] make Data.List.Base.[_] a pattern synonym breaking discussion library-design naming refactoring
#3095 opened Jul 30, 2026 by jamesmckinna Collaborator Loading…
4 of 5 tasks
7
[ refactor ] rename constructors of Data.List.Base.InitLast and friends breaking cosmetic deprecation refactoring status: blocked-by-issue Progress on this issue or PR is blocked by another issue. style-guide
#3090 opened Jul 26, 2026 by jamesmckinna Collaborator Loading… v3.0
1
strengthen the AVL tree's insertWith-just breaking refactoring
#3087 opened Jul 23, 2026 by mikedelorimier Contributor Loading…
9
Add colour to defunct-readme.sh and ignore .git
#3086 opened Jul 23, 2026 by silas-hw Contributor Loading…
2
[ refactor ] generalise Data.Sum.Relation.Binary.Pointwise.elim #3079 addition refactoring
#3085 opened Jul 23, 2026 by jamesmckinna Collaborator Loading… v3.0
8
Add Queue datatype
#3084 opened Jul 20, 2026 by silas-hw Contributor • Draft
1
122
Add defunct-readme check to CI
#3080 opened Jul 16, 2026 by silas-hw Contributor Loading…
1
1
[ add ] Pointwise lifting of algebra to Data.Vec.Functional addition
#3077 opened Jul 16, 2026 by JacquesCarette Collaborator Loading…
6
[ draft ] Refactor Dec to use constructive negation refactoring
#3065 opened Jul 9, 2026 by gallais Member • Draft v3.0
12
[ add ] syntax for antisym equality reasoning in Relation.Binary.Reasoning.PartialOrder #3047 addition low-hanging-fruit priority:lo
#3057 opened Jul 8, 2026 by jamesmckinna Collaborator Loading…
1
6
[ add ] Data.List.Base.foldMap and refactor addition refactoring
#3026 opened Jun 20, 2026 by jamesmckinna Collaborator Loading…
2 tasks done
v3.0
1
12
[ add ] Natural number square root addition
#3023 opened Jun 18, 2026 by jamesmckinna Collaborator • Draft
1
14
Make final parameter of Acc an index discussion mikan
#3020 opened Jun 18, 2026 by Taneb Member • Draft
8
Make irrelevant-recompute unsafe
#3012 opened Jun 10, 2026 by jespercockx Member Loading…
2 tasks
8
Add definitions for function-like relations addition
#3001 opened Jun 5, 2026 by Taneb Member Loading…
2
Replace irrelevance with Prop
#2998 opened May 27, 2026 by jespercockx Member • Draft
17
[ fix ] #2865 for the remaining Data.*.Relation.Unary.Any deprecation naming
#2972 opened Apr 1, 2026 by jamesmckinna Collaborator • Draft
5 tasks done
4
[Add] Division properties for Nat, Integer, and Rational addition
#2962 opened Mar 5, 2026 by aortega0703 Contributor Loading…
17
[Add] Properties of rounding in Rational
#2953 opened Feb 25, 2026 by aortega0703 Contributor Loading…
34
[ add ] left- and right- actions induced by a Magma homomorphism addition library-design
#2894 opened Nov 24, 2025 by jamesmckinna Collaborator • Draft
9
ProTip! Type g p on any issue or pull request to go back to the pull request listing page.