Skip to content

Pull requests: agda/agda-stdlib

New pull request New
65 Open 1,758 Closed
65 Open 1,758 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

Make irrelevant-recompute and corollaries unsafe
#3012 opened Jun 10, 2026 by jespercockx Member Loading…
2 tasks
1
Add Properties of List actions on Bools
#3005 opened Jun 8, 2026 by Taneb Member Loading…
1
Add properties relating Vec.lookup to head and tail
#3004 opened Jun 8, 2026 by Taneb Member Loading…
8
Add inverse assoc law to Data.List.Relation.Ternary.Appending.Setoid.Properties
#3002 opened Jun 6, 2026 by Taneb Member Loading…
4
Add definitions for function-like relations
#3001 opened Jun 5, 2026 by Taneb Member Loading…
1
Add O(1) native structural Binomial Theorem for Nat addition
#3000 opened Jun 2, 2026 by alfredoVallejoM Loading…
1
Replace irrelevance with Prop
#2998 opened May 27, 2026 by jespercockx Member • Draft
16
Add more Data.Rational.Properties
#2996 opened May 8, 2026 by kleinreact Loading…
7
Add Linked predicate transformer for guarded streams
#2993 opened May 4, 2026 by Taneb Member Loading… v3.0
2
[ new ] Data.SnocList.Base (re #2684) addition bug
#2982 opened Apr 16, 2026 by gallais Member Loading…
1
11
[ fix ] #2865 for the remaining Data.*.Relation.Unary.Any deprecation naming
#2972 opened Apr 1, 2026 by jamesmckinna Collaborator • Draft
5 tasks done
4
[ refactor ] downstream improvements following #2961 / #2968 refactoring status: blocked-by-issue Progress on this issue or PR is blocked by another issue.
#2970 opened Mar 25, 2026 by jamesmckinna Collaborator • Draft
6
Restore --without-K
#2967 opened Mar 20, 2026 by Taneb Member Loading… v3.0
8
[ refactor ] introduce revised notation for decidability of Lexicographic orderings, plus knock-ons deprecation refactoring
#2963 opened Mar 9, 2026 by jamesmckinna Collaborator • Draft
7
[Add] Division properties for Nat, Integer, and Rational
#2962 opened Mar 5, 2026 by aortega0703 Contributor • Draft
8
[ refactor ] name of Data.Product.Relation.Binary.Pointwise.NonDependent.×-decidable deprecation refactoring
#2958 opened Mar 2, 2026 by jamesmckinna Collaborator • Draft
13
[Add] Properties of rounding in Rational
#2953 opened Feb 25, 2026 by aortega0703 Contributor • Draft
31
[ breaking ] change fieldname _≟_ to _≈?_ in IsDecEquivalence breaking deprecation library-design refactoring style-guide
#2952 opened Feb 25, 2026 by jamesmckinna Collaborator • Draft v3.0
1
23
[ add ] left- and right- actions induced by a Magma homomorphism addition library-design
#2894 opened Nov 24, 2025 by jamesmckinna Collaborator • Draft
9
Attempt at the INT construction
#2891 opened Nov 23, 2025 by Taneb Member • Draft
1
22
[ draft ] Alternative design for sub- and quotient- (Abelian)Groups addition library-design refactoring
#2859 opened Nov 5, 2025 by jamesmckinna Collaborator • Draft
30
Add principal ideal construction
#2857 opened Nov 3, 2025 by Taneb Member • Draft
8
Add ideals and quotient rings
#2855 opened Oct 31, 2025 by Taneb Member • Draft
30
Normal subgroups and quotient groups
#2854 opened Oct 31, 2025 by Taneb Member Loading…
41
[ add ] Data.Bool.contradiction fixing #2847 addition
#2853 opened Oct 30, 2025 by jamesmckinna Collaborator • Draft
2
ProTip! Type g p on any issue or pull request to go back to the pull request listing page.