Skip to content

Pull requests: agda/agda-stdlib

New pull request New
34 Open 1,432 Closed
34 Open 1,432 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
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Pull requests list

Add properties/structures/bundles related to decidability for Relation.Binary.Construct.Interior.Symmetric addition refactoring
#2481 opened Sep 11, 2024 by jamesmckinna Loading… v2.2
4
Lists: porting several lemmas from other libraries addition naming
#2479 opened Sep 10, 2024 by omelkonian Loading… v2.2
54
fixes #2466: add equivalence proofs addition cosmetic refactoring
#2478 opened Sep 9, 2024 by jamesmckinna Loading… v2.2
1
1
Replace record directive "eta-equality" by "no-eta-equality;pattern" breaking upstream Changes induced by Agda upstream
#2476 opened Sep 6, 2024 by andreasabel • Draft Agda v2.8.0
6
Rename homo to ∙-homo in Algebra.Morphism.Structures breaking cosmetic deprecation naming refactoring
#2464 opened Aug 29, 2024 by jamesmckinna Loading… v3.0
1
9
Define strictify function at each base type, plus evident property low-hanging-fruit refactoring
#2459 opened Aug 15, 2024 by jamesmckinna • Draft
8
Refactor Algebra.Solver.*Monoid (further!) deprecation refactoring
#2457 opened Aug 14, 2024 by jamesmckinna • Draft
1
9
Add new Bool action on a RawMonoid plus properties addition
#2450 opened Jul 31, 2024 by jamesmckinna • Draft
15
Implement ≤-total in terms of _≤?_ breaking performance refactoring
#2440 opened Jul 19, 2024 by Taneb Loading…
1
19
Vec.Properties: drop eq parameter when it is a property (v3.0 changes) breaking refactoring
#2431 opened Jul 5, 2024 by mildsunrise • Draft v3.0
Vec.Properties: introduce ≈-cong′ addition
#2424 opened Jul 1, 2024 by mildsunrise • Draft v2.2
15
Add some type relations and isomorphisms addition
#2419 opened Jun 24, 2024 by WhatisRT Loading… v2.2
16
Fix #2396 by removing redundant zero in IsNonAssociativeRing breaking bug refactoring
#2410 opened Jun 16, 2024 by lexvanderstoep • Draft v3.0
5
Add Number literals for any SuccessorSet addition library-design low-hanging-fruit
#2406 opened Jun 10, 2024 by jamesmckinna Loading… v2.2
1
13
Add bundled homomorphisms addition
#2383 opened May 8, 2024 by jamesmckinna Loading…
3 tasks done
v2.2
1
40
[ 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
remove everything deprecated from v1.3 (and before) breaking deprecation
#2338 opened Apr 1, 2024 by JacquesCarette Loading… v3.0
9
Refactor Data.List.Relation.Binary.Permutation.*, part I addition refactoring
#2333 opened Mar 28, 2024 by jamesmckinna Loading… v2.2
1
49
Refactor Data.List.Relation.Binary.Permutation.* addition breaking dependencies discussion refactoring
#2317 opened Mar 12, 2024 by jamesmckinna • Draft
13
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 Loading…
8 tasks done
40
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
ProTip! Updated in the last three days: updated:>2024-09-20.