Skip to content

Pull requests: agda/agda-stdlib

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

Pull requests list

Refactor Data.List.Base.scan* and their properties addition dependencies deprecation refactoring
#2395 opened May 23, 2024 by jamesmckinna Loading… v2.1
1
Add the Setoid-based Monoid on (List, [], _++_) addition library-design refactoring
#2393 opened May 21, 2024 by jamesmckinna Loading… v2.1
1
2
style-guide rule for initial private block in modules documentation style-guide
#2392 opened May 20, 2024 by jamesmckinna Loading…
1
2
More list properties about catMaybes/mapMaybe addition
#2389 opened May 17, 2024 by omelkonian Loading…
59
Add bundled homomorphisms addition low-hanging-fruit
#2383 opened May 8, 2024 by jamesmckinna Loading…
3 tasks done
v2.1
1
31
Adapt to reflection interface changes reflection upstream
#2380 opened May 4, 2024 by cmcmA20 • Draft Agda-2.6.5
4
[ new ] Word8, Bytestring, Bytestring builder
#2376 opened May 1, 2024 by gallais • Draft
1 task
5
Very dependent map addition
#2373 opened Apr 24, 2024 by JacquesCarette Loading… v2.1
1
22
[ new ] Effect.Monad.Random addition
#2372 opened Apr 22, 2024 by gallais • Draft
2 tasks
Improve Data.List.Base (fix #2359; deprecate use of with #2123) cosmetic library-design refactoring
#2366 opened Apr 15, 2024 by jamesmckinna Loading… v2.1
5
Add Algebra.Action.* and friends addition library-design status: blocked-by-issue Progress on this issue or PR is blocked by another issue.
#2350 opened Apr 9, 2024 by jamesmckinna • Draft
5 tasks done
1
114
Port two Endomorphism submodules over to new Function hierarchy addition refactoring
#2342 opened Apr 3, 2024 by JacquesCarette Loading… v2.1
1
58
remove everything deprecated from v1.3 (and before) breaking deprecation
#2338 opened Apr 1, 2024 by JacquesCarette Loading… v3.0
9
Implement move-via-deprecate of decToMaybe as per #2330 dependencies deprecation low-hanging-fruit refactoring
#2336 opened Mar 29, 2024 by JacquesCarette Loading… v2.1
1
20
Refactor Data.List.Relation.Binary.Permutation.*, part I addition refactoring
#2333 opened Mar 28, 2024 by jamesmckinna Loading… v2.1
1
47
Refactor List.Membership.* and List.Relation.Unary.Any addition cosmetic dependencies refactoring
#2324 opened Mar 21, 2024 by jamesmckinna Loading… v2.1
63
Refactor Data.List.Relation.Binary.Permutation.* addition breaking dependencies discussion refactoring
#2317 opened Mar 12, 2024 by jamesmckinna • Draft
10
Add Effect.Foldable and Data.List.Effectful.Foldable implementation addition discussion library-design
#2300 opened Feb 23, 2024 by jamesmckinna • Draft
14
Modular arithmetic based on Data.Nat.Bounded #2257 addition discussion library-design
#2292 opened Feb 12, 2024 by jamesmckinna • Draft
3
Consequences of module monomorphisms
#2276 opened Feb 3, 2024 by Taneb • Draft
2 of 8 tasks
10
Remove (almost!) all external use of _≤″_ beyond Data.Nat.* dependencies refactoring
#2262 opened Jan 21, 2024 by jamesmckinna Loading… v2.1
21
Add Data.Nat.Bounded addition low-hanging-fruit
#2257 opened Jan 15, 2024 by jamesmckinna Loading…
28
Adds Relation.Nullary.Recomputable plus consequences addition library-design
#2243 opened Jan 2, 2024 by jamesmckinna Loading…
3 tasks done
v2.1
1
53
WIP Add Rational RingSolver addition
#2215 opened Nov 26, 2023 by lemastero • Draft
3 of 5 tasks
1
9
Enhancement to Relation.Nullary.Reflects etc. addition refactoring status: blocked-by-issue Progress on this issue or PR is blocked by another issue.
#2149 opened Oct 13, 2023 by jamesmckinna • Draft
4 tasks
14
ProTip! no:milestone will show everything without a milestone.