Skip to content

Issues: agda/agda

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

Clear current search query, filters, and sorts
40 Open 183 Closed
40 Open 183 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

Loss of context in checkType primitive aim Issue/PR stemming from AIM (Agda Implementor's Meeting) forcing Forcing analysis and forcing translation of clauses reflection Elaborator reflection, macros, tactic arguments
#7630 opened Nov 29, 2024 by WhatisRT
2
Compatibiilty of partial elements defined using cubical face lattice generators with reflextion machinery cubical Cubical Agda paraphernalia: Paths, Glue, partial elements, hcomp, transp reflection Elaborator reflection, macros, tactic arguments type: enhancement Issues and pull requests about possible improvements
#7288 opened May 22, 2024 by marcinjangrzybowski 2.8.0
Defining local helper functions in reflection reflection Elaborator reflection, macros, tactic arguments
#7056 opened Jan 8, 2024 by ncfavier
GeneralizeTel shows up in error message generalize Related to generalisable variables reflection Elaborator reflection, macros, tactic arguments type: bug Issues and pull requests about actual bugs
#6951 opened Nov 2, 2023 by jespercockx icebox
1
Non-dependent tactic argument fails to run tactic parser Problems with the parser's implementation (rather than with decisions about syntax) reflection Elaborator reflection, macros, tactic arguments tactic tactic annotations type: bug Issues and pull requests about actual bugs
#6939 opened Oct 23, 2023 by jespercockx later
@andreasabel
7
Detecting transpX in reflection cubical Cubical Agda paraphernalia: Paths, Glue, partial elements, hcomp, transp reflection Elaborator reflection, macros, tactic arguments type: enhancement Issues and pull requests about possible improvements
#6840 opened Sep 11, 2023 by ncfavier later
Reflection fails to normalise self-referencing copattern lambda extended lambdas Pattern matching lambda expressions, Cubical Agda "system literals" reflection Elaborator reflection, macros, tactic arguments type: bug Issues and pull requests about actual bugs
#6839 opened Sep 11, 2023 by ncfavier icebox
1
inferType doesn't check enough reflection Elaborator reflection, macros, tactic arguments
#6585 opened Apr 22, 2023 by ncfavier icebox
1
Allow reflection primitives to access erased things erasure reflection Elaborator reflection, macros, tactic arguments type: enhancement Issues and pull requests about possible improvements
#6400 opened Dec 9, 2022 by jespercockx later
@jespercockx
Feature proposal: Partial static functions for instance search and metaprogramming instance Instance resolution reflection Elaborator reflection, macros, tactic arguments rewriting Rewrite rules, rewrite rule matching type: discussion Discussions about Agda's design and implementation type: enhancement Issues and pull requests about possible improvements
#6378 opened Dec 2, 2022 by jespercockx later
3
Make reflection well-scoped wrt. de Bruijn indices de-Bruijn Internal problems with variable scoping ("de Bruijn indices") reflection Elaborator reflection, macros, tactic arguments
#6317 opened Nov 10, 2022 by andreasabel later
Elaborate-and-give does not update precedence without reload agda-mode Issues relating to the Emacs agda2-mode reflection Elaborator reflection, macros, tactic arguments type: bug Issues and pull requests about actual bugs ux: interaction Issues to do with interactive development (holes, case splitting, etc)
#6209 opened Oct 19, 2022 by plt-amy icebox
1
Internal errors due to use of runSpeculative reflection Elaborator reflection, macros, tactic arguments type: bug Issues and pull requests about actual bugs
#6125 opened Sep 22, 2022 by nad later
3
Reflection mechanism for rewriting reflection Elaborator reflection, macros, tactic arguments rewriting Rewrite rules, rewrite rule matching type: enhancement Issues and pull requests about possible improvements
#6088 opened Sep 6, 2022 by Trebor-Huang later
4
Reflection primitives turning TC into a reader and state monad PR welcome Welcome to submit a PR fixing this issue reflection Elaborator reflection, macros, tactic arguments type: enhancement Issues and pull requests about possible improvements
#5873 opened Apr 26, 2022 by WhatisRT icebox
Redesign syntax for unquoting declarations reflection Elaborator reflection, macros, tactic arguments type: enhancement Issues and pull requests about possible improvements
#5864 opened Apr 14, 2022 by L-TChen later
@L-TChen
4
Freshly generated instance by reflection cannot be searched instance Instance resolution PR welcome Welcome to submit a PR fixing this issue reflection Elaborator reflection, macros, tactic arguments scope Issues relating to scope checking type: enhancement Issues and pull requests about possible improvements
#5757 opened Jan 26, 2022 by L-TChen icebox
5
Reflection: termination of generated instance reflection Elaborator reflection, macros, tactic arguments termination Issues relating to the termination checker type: bug Issues and pull requests about actual bugs
#5747 opened Jan 17, 2022 by omelkonian later
@jespercockx
4
Reflection: cannot programmatically give refl reflection Elaborator reflection, macros, tactic arguments type: enhancement Issues and pull requests about possible improvements
#5738 opened Jan 14, 2022 by omelkonian icebox
6
Weird error (and weird location) with tactic on hidden argument reflection Elaborator reflection, macros, tactic arguments tactic tactic annotations type: bug Issues and pull requests about actual bugs
#5423 opened May 31, 2021 by andreasabel later
Reflection on modules modules Issues relating to the module system reflection Elaborator reflection, macros, tactic arguments type: enhancement Issues and pull requests about possible improvements
#5399 opened May 19, 2021 by laMudri icebox
10
Add annotations for definitions generated by reflection PR welcome Welcome to submit a PR fixing this issue reflection Elaborator reflection, macros, tactic arguments type: enhancement Issues and pull requests about possible improvements
#4698 opened May 30, 2020 by WhatisRT icebox
8
[reflection] Get list of all available definitions? reflection Elaborator reflection, macros, tactic arguments type: enhancement Issues and pull requests about possible improvements
#4581 opened Apr 12, 2020 by t-more icebox
4
Delay execution of macros. reflection Elaborator reflection, macros, tactic arguments type: enhancement Issues and pull requests about possible improvements
#4198 opened Nov 15, 2019 by xekoukou icebox
@xekoukou
3
Reflect on the constraints. constraints Constraints (postponed type checking problems, postponed unification problems, instance constraints) reflection Elaborator reflection, macros, tactic arguments type: enhancement Issues and pull requests about possible improvements
#4171 opened Nov 4, 2019 by xekoukou icebox
@xekoukou
1
ProTip! Updated in the last three days: updated:>2025-01-16.