Skip to content

Pull requests: agda/agda-stdlib

New pull request New
53 Open 1,655 Closed
53 Open 1,655 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

Add cartesianProductWith⁻ and cartesianProduct⁻ to All
#2824 opened Sep 3, 2025 by javierdiaz72 Loading…
4
[ add ] PartialOrder structure/bundle on _→_ (fixes issue #2820) addition
#2823 opened Aug 31, 2025 by jamesmckinna Loading…
1
1
[bug] replace wrong argument to projection in Algebra.Morphism.Construct.DirectProduct bug
#2822 opened Aug 29, 2025 by carlostome Loading…
1
[draft] Polynomial
#2821 opened Aug 29, 2025 by samparkky • Draft
11
[ add ] Pointwise lifting of algebra to Data.Vec.Functional (Functional vector module #1945 redux)
#2817 opened Aug 28, 2025 by e-mniang Loading…
22
[ add ] Setoid from PartialSetoid addition subsets relies on/infleunced by/influences, various approaches to the notion of 'subset(oid)' in type theory
#2816 opened Aug 24, 2025 by jamesmckinna • Draft
22
Add new module Effect.Functor.Naperian - Continuation of #2004
#2815 opened Aug 22, 2025 by gabriellisboaconegero Loading…
23
[ add ] Pointed extension of an ordering addition
#2813 opened Aug 20, 2025 by jamesmckinna Loading…
5
Module morphisms polymorphic in the underlying ring structure
#2810 opened Aug 15, 2025 by Taneb • Draft
3 of 4 tasks
4
[Add] Initial files for Domain theory - Continuation of #2721
#2809 opened Aug 13, 2025 by gabriellisboaconegero Loading…
28
[ refactor ] Data.List.Relation.Binary.Sublist.Propositional.Properties addition breaking
#2808 opened Aug 13, 2025 by jamesmckinna • Draft
10
[ refactor ] reorganise Relation.Nullary.Negation.Core to make clean separation of properties cosmetic dependencies refactoring
#2805 opened Aug 5, 2025 by jamesmckinna Loading… v2.4
3
[ refactor ] make contradiction and friends entirely definitionally proof-irrelevant breaking discussion library-design refactoring status: blocked-by-issue Progress on this issue or PR is blocked by another issue.
#2802 opened Aug 4, 2025 by jamesmckinna • Draft
5 tasks
v3.0
19
[ add ] clean version of Data.Fin.Properties.searchMinimalCounterexample addition refactoring
#2801 opened Aug 2, 2025 by jamesmckinna Loading… v2.4
7
[ add ] flipped version of Relation.Nullary.Negation.Core.contradiction addition refactoring
#2797 opened Jul 31, 2025 by jamesmckinna Loading… v2.4
1
2
[add] partial elements in Effect.Monad.Partial module
#2796 opened Jul 30, 2025 by e-mniang • Draft
26
[Add] truncate properties to Data.Vec.Properties addition
#2795 opened Jul 30, 2025 by e-mniang Loading… v2.4
32
[ refactor ] Data.Fin.Properties.decFinSubset cosmetic refactoring
#2793 opened Jul 30, 2025 by jamesmckinna Loading… v2.4
4
[ refactor ] make i ≢ j argument to Data.Fin.Base.punchOut irrelevant breaking refactoring
#2790 opened Jul 28, 2025 by jamesmckinna Loading… v3.0
6
[ refactor ] make m ≤ n argument to Data.Vec.Base.{truncate|padRight} irrelevant breaking refactoring status: blocked-by-issue Progress on this issue or PR is blocked by another issue.
#2787 opened Jul 27, 2025 by jamesmckinna Loading… v3.0
1
2
[ refactor ] make n≢i : n ≢ toℕ i argument to lower₁ irrelevant breaking refactoring
#2783 opened Jul 25, 2025 by jamesmckinna Loading… v3.0
14
[ refactor ] Data.Fin.Properties following #2746 refactoring
#2782 opened Jul 25, 2025 by jamesmckinna Loading… v2.4
4
Ring reasoning addition
#2765 opened Jul 12, 2025 by JacquesCarette • Draft v2.4
11
[ add ] BooleanRing plus Properties addition
#2763 opened Jul 10, 2025 by jamesmckinna Loading…
3 of 4 tasks
v2.4
1
15
[ discussion ] alternative design for Algebra.Structures.IsX and Algebra.Properties.X addition dependencies discussion library-design refactoring
#2762 opened Jul 9, 2025 by jamesmckinna • Draft hypothetical-rewrite
2
ProTip! Follow long discussions with comments:>50.