Skip to content

Pull requests: agda/agda

New pull request New
54 Open 2,549 Closed
54 Open 2,549 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

[ fix #8557 ] Only resurrect irrelevant variables once
#8576 opened May 28, 2026 by jespercockx Member • Draft 2.9.0
Add flag for irrelevance irrelevance Issues to do with irrelevance annotations type: enhancement Issues and pull requests about possible improvements ux: options Issues relating to Agda's command line options
#8575 opened May 25, 2026 by jespercockx Member Loading… 2.9.0
Allow casing on props when the pattern has absurd sub-patterns absurd clauses Absurd patterns, absurd extended lambdas, absurd clauses in definitions pr: squash-me This PR needs squashing prop Prop, definitional proof irrelevance type: enhancement Issues and pull requests about possible improvements
#8548 opened May 2, 2026 by Soares Contributor Loading… 2.9.0
1
23
Guarded TT: move part of LaterPrims to Agda.Primitive and test/Common builtin Enhancements to the builtin modules and builtin definitions guarded cubical Guarded Cubical Agda
#8517 opened Apr 18, 2026 by anuyts Contributor Loading…
7
Tastify interaction suite infra: test suite Issues relating to the test suite (not in changelog) platform: nix Building and running with Nix/NixOS pr: preserve commits PR should be merged via rebase, preserving the commits ux: interaction Issues to do with interactive development (holes, case splitting, etc)
#8513 opened Apr 17, 2026 by lawcho Collaborator • Draft
9
Add CONTRIBUTING.md
#8507 opened Apr 16, 2026 by jespercockx Member Loading…
4
Occurs checking refactoring occurs check Problems with checking that metavariable solutions aren't loopy performance Slow type checking, interaction, compilation or execution of Agda programs refactor Changes to the code base which do not affect users (not in changelog)
#8497 opened Apr 13, 2026 by AndrasKovacs Collaborator Loading…
1
3
Fall back to hole range when refine input has no range interaction-json JSON protocol for communicating with Agda
#8493 opened Apr 9, 2026 by dancewithheart Contributor Loading… 2.10.0
2
10
Disambiguate module & other names in JS output backend: js JavaScript generation backend
#8484 opened Mar 27, 2026 by lawcho Collaborator Loading… 2.10.0
1
Add C main to configure RTS. performance Slow type checking, interaction, compilation or execution of Agda programs
#8482 opened Mar 26, 2026 by wenkokke Contributor Loading… 2.10.0
16
Delete sortRulesOfSymbol confluence Concerning confluence of rewriting. rewriting Rewrite rules, rewrite rule matching status: work-in-progress Do not merge ATM
#8464 opened Mar 9, 2026 by NathanielB123 Member Loading…
1
Erased levels [cubical]
#8461 opened Mar 5, 2026 by nad Collaborator • Draft 2.10.0
@nad
2
Track module usage in -WUnusedImports warnings
#8272 opened Dec 8, 2025 by Copilot AI • Draft
@andreasabel
Update -WUnusedImports to take modules into consideration import Issues to do with importing modules maculata Issue with a so far unreleased feature (not in changelog) ux: warnings Issues relating to the reporting of warnings
#8271 opened Dec 8, 2025 by andreasabel Member • Draft 2.9.0
2
More semantic structure of html generated from agda files
#8241 opened Nov 29, 2025 by marcinjangrzybowski Contributor • Draft
AST based navigation/interaction in emacs
#8219 opened Nov 24, 2025 by marcinjangrzybowski Contributor • Draft
1
Generate parts of the Agda input method procedurally ux: emacs Issues relating to the Emacs agda2-mode
#8180 opened Nov 1, 2025 by phikal Contributor Loading… 2.10.0
15
Double-checking meta solutions: fail hard on errors
#8061 opened Aug 9, 2025 by andreasabel Member • Draft
WIP: so far failing attempt at #7656 help wanted
#7844 opened May 1, 2025 by andreasabel Member • Draft
1
[opt] Lazy 'dontUnfold' in unfoldDefinition reduction status: do-not-merge So please don't merge
#7821 opened Apr 28, 2025 by andreasabel Member • Draft
Prefer name hints from constructor definitions type: discussion Discussions about Agda's design and implementation ux: case splitting Issues relating to the case split ("C-c C-c") command ux: interaction Issues to do with interactive development (holes, case splitting, etc) ux: printing Issues relating to how terms are printed for display
#7754 opened Mar 21, 2025 by lawcho Collaborator • Draft
8
Issue #7714: New cabal flag -f Werror to control -Werror build Concerning building of Agda release Concerning the release process and releases (not in changelog)
#7718 opened Feb 20, 2025 by andreasabel Member • Draft 2.9.0
1
@andreasabel
7
WIP: make agda-tests into its own package
#7717 opened Feb 20, 2025 by andreasabel Member • Draft
Implement checkInternal for definitions aim Issue/PR stemming from AIM (Agda Implementor's Meeting) checkInternal Bugs with, or caught by, the internal double-checker status: work-in-progress Do not merge ATM type: enhancement Issues and pull requests about possible improvements type-checking
#7628 opened Nov 29, 2024 by liesnikov Contributor • Draft
3 tasks
@liesnikov
Passing string with error in catchTC
#7623 opened Nov 26, 2024 by marcinjangrzybowski Contributor • Draft
1
ProTip! Find all pull requests that aren't related to any open issues with -linked:issue.