Skip to content

Pull requests: agda/agda

New pull request New
45 Open 1,794 Closed
45 Open 1,794 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

Overhaul dead code elimination, make --save-metas the default
#7248 opened May 5, 2024 by AndrasKovacs Loading…
1
Reflection & erasure, improving quality of life
#7247 opened May 4, 2024 by cmcmA20 Loading…
1
Instantiate terms before traversing them in tcExtendContext
meta Metavariables, insertion of implicit arguments, etc reflection Elaborator reflection, macros, tactic arguments
#7231 opened Apr 20, 2024 by ncfavier Loading…
1
9
Re #7163: test installing with --enable-executable-dynamic in CI
Setup.hs Concerning the Custom build type of Agda status: do-not-merge So please don't merge ux: installation Getting Agda set up on your machine
#7172 opened Mar 6, 2024 by andreasabel Loading…
1
Re #6097: checkApplication: retry check target analysis less eagerly.
performance Slow type checking, interaction, compilation or execution of Agda programs type-checking
#7171 opened Mar 6, 2024 by andreasabel • Draft
1
1
Add -*- lexical-binding: t; -*- to the first lines of agda-mode files
#7166 opened Mar 5, 2024 by VitalyAnkh • Draft
Migrate tests to Agda.cabal
cabal Build problems specifically related to cabal-install infra: test suite Issues relating to the test suite (not in changelog) Makefile Concerning the Makefile that builds Agda (not in changelog) refactor Changes to the code base which do not affect users (not in changelog) status: work-in-progress Do not merge ATM
#7165 opened Mar 4, 2024 by lawcho • Draft
2
Fix #6866: User Manual: Make Installation as Easy as Possible
#7155 opened Feb 29, 2024 by AJChapman Loading… 2.7.0
7
Add type-based termination checker
pr: squash-me This PR needs squashing termination Issues relating to the termination checker
#7152 opened Feb 27, 2024 by knisht Loading… 2.7.0
@andreasabel
39
Janitorial changes to the Emacs mode (Take 2)
pr: preserve commits PR should be merged via rebase, preserving the commits
#7140 opened Feb 21, 2024 by phikal Loading…
2
Eta record refactorings
refactor Changes to the code base which do not affect users (not in changelog)
#7132 opened Feb 18, 2024 by jespercockx Loading… 2.7.0
1
Fix #6262: Makefile: remove prerequisite install-deps and -no-deps goals
#7117 opened Feb 14, 2024 by andreasabel Loading… 2.7.0
1
11
Move unicode keybindings into JSON file
agda-mode Issues relating to the Emacs agda2-mode pr: squash-me This PR needs squashing refactor Changes to the code base which do not affect users (not in changelog) unicode ux: emacs Issues relating to the Emacs agda2-mode
#7094 opened Feb 7, 2024 by lawcho Loading…
1
[ fix #6384 ] Use Alpine Linux to compile and statically link Agda
#7082 opened Feb 2, 2024 by L-TChen Loading… 2.7.0
1
6
comment cubical
#7068 opened Jan 24, 2024 by andreasabel Loading…
Add ⧺ in agda-input.el
#7023 opened Dec 8, 2023 by AlexD97 Loading…
Check the section application in noMutualBlock
let Issues relating to let expressions modules Issues relating to the module system mutual pr: squash-me This PR needs squashing status: do-not-merge So please don't merge
#7014 opened Nov 29, 2023 by andreasabel Loading… 2.7.0
6
[new] backend-end specific interaction
agda-mode Issues relating to the Emacs agda2-mode backends
#7010 opened Nov 24, 2023 by omelkonian • Draft
2
Restore cabal.project
#6993 opened Nov 13, 2023 by andreasabel • Draft
4
[ #6934 ] Added --opaque and the keyword transparent
opaque Issues about `opaque` definitions status: do-not-merge So please don't merge ux: options Issues relating to Agda's command line options
#6979 opened Nov 10, 2023 by nad • Draft 2.7.0
1
@nad
Expose the names of generated record constructors
record constructors Issues involving record constructors.
#6975 opened Nov 9, 2023 by plt-amy • Draft 2.7.0
2
[ fix #5315 ] Remove erased and irrelevant arguments completely in GHC backend
#6928 opened Oct 19, 2023 by jespercockx • Draft
1
2
Reopen PR "Add record where syntax sugar (#6603)"
record expression Issues concerning record{...} expressions (record literals and record updates) type: enhancement Issues and pull requests about possible improvements
#6911 opened Oct 9, 2023 by andreasabel • Draft 2.7.0
@andreasabel
1
Declare dependency blaze-markup directly to utilize toHtml for String1
backend: html HTML generation backend
#6883 opened Sep 26, 2023 by andreasabel • Draft later
1
explicit imports and inline types example: Agda.Utils.Empty
refactor Changes to the code base which do not affect users (not in changelog) style Haskell coding style (not in changelog)
#6859 opened Sep 16, 2023 by pnlph • Draft
4
ProTip! no:milestone will show everything without a milestone.