Skip to content

Pull requests: agda/agda-stdlib

New pull request New
27 Open 1,388 Closed
27 Open 1,388 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

Add IsIdempotentMonoid and IsCommutativeBand to Algebra.Structures addition dependencies library-design low-hanging-fruit
#2402 opened Jun 5, 2024 by jamesmckinna Loading… v2.1
1
3
Add bundled homomorphisms addition
#2383 opened May 8, 2024 by jamesmckinna Loading…
3 tasks done
v2.2
1
34
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
[ new ] Effect.Monad.Random addition
#2372 opened Apr 22, 2024 by gallais • Draft
2 tasks
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
2
63
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
23
Refactor Data.List.Relation.Binary.Permutation.*, part I addition refactoring
#2333 opened Mar 28, 2024 by jamesmckinna Loading… v2.2
1
47
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
26
Add Data.Nat.Bounded addition low-hanging-fruit
#2257 opened Jan 15, 2024 by jamesmckinna Loading… v2.2
28
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
Numeric non-zero equivalents/Redesign of Almost* properties in Algebra.Definitions addition breaking deprecation discussion instances library-design naming
#2117 opened Sep 30, 2023 by jamesmckinna • Draft
11
Added Z mod n as Fin addition
#2073 opened Aug 27, 2023 by guilhermehas Loading… v2.2
64
[ new ] notions of finiteness
#2022 opened Jul 13, 2023 by Saransh-cpp Loading…
3
[ new ] notions of finiteness
#2017 opened Jul 9, 2023 by laMudri Loading…
12 tasks
27
Add new module Effect.Functor.Naperian addition paper-based
#2004 opened Jun 22, 2023 by Sofia-Insa • Draft
31
The free Magma on a Set, resp. Setoid [bis] addition discussion library-design naming status: blocked-by-issue Progress on this issue or PR is blocked by another issue.
#1962 opened May 1, 2023 by jamesmckinna Loading…
62
Functional vector module
#1945 opened Apr 17, 2023 by guilhermehas • Draft
14
ProTip! Add no:assignee to see everything that’s not assigned.