Skip to content

Issues: agda/agda-stdlib

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

229 Open 804 Closed
229 Open 804 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
Assignee
Filter by who’s assigned
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Issues list

lib-2.1.1: unused import in ...All/Properties.agda refactoring
#2533 opened Dec 23, 2024 by mechvel
1
[ refactor ] Reconcile left/right congruence statements and proofs breaking
#2532 opened Dec 22, 2024 by jamesmckinna v3.0
3
Inconvenient precedences breaking bug library-design
#2531 opened Dec 20, 2024 by JacquesCarette
7
Add ⊆-Reasoning module/combinators for Data.List.Relation.Binary.Sublist.* addition library-design
#2526 opened Dec 19, 2024 by jamesmckinna
1
[ refactor ] Functoriality of Data.List.Relation.Binary.Sublist|Subset wrt All and Any addition dependencies refactoring
#2525 opened Dec 18, 2024 by jamesmckinna
3
The type of a data constructor should *not* have repeated indices unless defined within the scope of with-K cubical-compatible supersedes `without-K` library-design style-guide
#2519 opened Dec 12, 2024 by jamesmckinna
5
[ refactor ] Possible refactoring of #2509 / #2513 ? refactoring
#2517 opened Dec 11, 2024 by jamesmckinna
1
5
Rename Data.List.Properties.*-is-foldr bikeshedding cosmetic deprecation library-design naming refactoring
#2516 opened Dec 11, 2024 by jamesmckinna v3.0
1
[ project ] merge PRs #2017 and #2022
#2511 opened Dec 6, 2024 by jamesmckinna
@JacquesCarette
1
Drop equivalence relation from Algebra.Bundles.Raw structures? discussion library-design
#2506 opened Nov 25, 2024 by carlostome hypothetical-rewrite
8
Refactor Algebra.Consequences.*? discussion library-design refactoring
#2502 opened Nov 22, 2024 by jamesmckinna v3.0
4
Problem with DISPLAY pragma for ⊥ in Data.Empty bug status: blocked-by-issue Progress on this issue or PR is blocked by another issue. upstream Changes induced by Agda upstream
#2493 opened Oct 4, 2024 by jamesmckinna Agda v2.8.0
6
[DRY] Refactor algebraic properties of types breaking dependencies library-design refactoring
#2489 opened Oct 1, 2024 by jamesmckinna v3.0
Runtime irrelevance
#2486 opened Sep 26, 2024 by kurnevsky
7
Add EquationalReasoning combinators for _∼[ set ]_?
#2483 opened Sep 18, 2024 by jamesmckinna
2
[DRY?] Direct definition vs. generic combinators, ctd. in Algebra.Definitions.RawMonoid addition performance question refactoring
#2475 opened Sep 5, 2024 by jamesmckinna
3
Find all single letter publicly-exported modules and make sure they are private breaking bug
#2472 opened Sep 3, 2024 by MatthewDaggitt v3.0
5
Relation.Binary.Definitions._Respects₂_ seems to exchange 'left' and 'right' in its left/right projections? breaking bug
#2471 opened Sep 2, 2024 by jamesmckinna v3.0
1
3
Get rid of inconsistent homo name in algebra hierarchy? breaking discussion naming
#2458 opened Aug 15, 2024 by jamesmckinna
1
5
Add Algebra.Definitions.RawGroup and Algebra.Properties.Group.* addition
#2454 opened Aug 1, 2024 by jamesmckinna
5
Deploy doc rendering for v2.1 admin continuous-integration release
#2452 opened Aug 1, 2024 by andreasabel v2.1
2
Refactor Data.Nat.GeneralisedArithmetic
#2446 opened Jul 29, 2024 by jamesmckinna
2
Linear-time implementation of Data.Nat.Properties.≤′⇒≤? addition discussion library-design performance refactoring
#2442 opened Jul 26, 2024 by jamesmckinna
3
Data.List.upTo/applyUpTo can be made faster performance refactoring
#2437 opened Jul 11, 2024 by Taneb
5
Data.Nat.Properties.≤-total should be implemented with _<ᵇ_ breaking bug performance refactoring
#2436 opened Jul 11, 2024 by Taneb
1
14
ProTip! Find all open issues with in progress development work with linked:pr.