-
Notifications
You must be signed in to change notification settings - Fork 337
Pull requests: agda/agda
Author
Label
Projects
Milestones
Reviews
Assignee
Sort
Pull requests list
New error warning CoinductiveEtaRecord instead of GenericError
coinduction
Coinductive records, musical coinduction
eta
η-expansion of metavariables and unification modulo η
ux: warnings
Issues relating to the reporting of warnings
Temporary fix for reflection of partial elements.
#7287
opened May 22, 2024 by
marcinjangrzybowski
Loading…
[refactor] __FROM_JUST__ = fromMaybe __IMPOSSIBLE__
refactor
Changes to the code base which do not affect users (not in changelog)
#7281
opened May 17, 2024 by
omelkonian
Loading…
Reflecting partial elements defined by extended lambdas
#7257
opened May 14, 2024 by
marcinjangrzybowski
•
Draft
[ GitHub ] Add Issues related to the closed-issues-for-milestone program (not in changelog)
infra: github workflows
Issues related to GitHub workflows and actions (not in changelog)
release.yml to format automatically generated release notes
closed-issues-for-milestone
#7254
opened May 14, 2024 by
L-TChen
Loading…
Overhaul dead code elimination, make --save-metas the default
#7248
opened May 5, 2024 by
AndrasKovacs
Loading…
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…
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…
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
Add
-*- lexical-binding: t; -*- to the first lines of agda-mode files
#7166
opened Mar 5, 2024 by
VitalyAnkh
•
Draft
Migrate tests to 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
Agda.cabal
cabal
Add type-based termination checker
pr: squash-me
This PR needs squashing
termination
Issues relating to the termination checker
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…
Eta record refactorings
refactor
Changes to the code base which do not affect users (not in changelog)
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…
Check the section application in 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
noMutualBlock
let
Previous Next
ProTip!
What’s not been updated in a month: updated:<2024-05-08.