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
34 Open 100 Closed
34 Open 100 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

Automatically create names for syntax import Issues to do with importing modules names scope Issues relating to scope checking
#7137 opened Feb 20, 2024 by MatthewDaggitt
Section variables are in scope of operator arguments mixfix Interaction between mixfix operators and other language features scope Issues relating to scope checking type: bug Issues and pull requests about actual bugs
#7041 opened Dec 23, 2023 by ncfavier
7
inverseScopeLookup gets much slower when --cubical-compatible is enabled cubical Cubical Agda paraphernalia: Paths, Glue, partial elements, hcomp, transp performance Slow type checking, interaction, compilation or execution of Agda programs scope Issues relating to scope checking
#6243 opened Oct 27, 2022 by plt-amy icebox
1
Check module equality before issuing "Ambiguous name" error ambiguous-names Issues to do with reporting of name ambiguity parameters Module parameters scope Issues relating to scope checking type: enhancement Issues and pull requests about possible improvements
#6035 opened Aug 18, 2022 by anuyts icebox
8
Inconsistent treatment of redeclarations of names modules Issues relating to the module system scope Issues relating to scope checking type: bug Issues and pull requests about actual bugs
#5976 opened Jun 25, 2022 by nad icebox
1
genTel shows up in context, meta-solution printed as _ generalize Related to generalisable variables scope Issues relating to scope checking type: bug Issues and pull requests about actual bugs ux: interaction Issues to do with interactive development (holes, case splitting, etc)
#5851 opened Mar 25, 2022 by andreasabel later
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
OperatorsExpr parsing blows up on large file operators Parsing of mixfix operators performance Slow type checking, interaction, compilation or execution of Agda programs scope Issues relating to scope checking type: bug Issues and pull requests about actual bugs
#5670 opened Nov 23, 2021 by AndrasKovacs 2.8.0
9
open public in a private block should not bring names into scope open-public private scope Issues relating to scope checking type: discussion Discussions about Agda's design and implementation
#5461 opened Jun 26, 2021 by jespercockx icebox
11
Weird scope checking of pattern synonyms (WAS: Backward jumps) language change Changes to the language which can be observed by Agda's userbase pattern-synonyms scope Issues relating to scope checking type: bug Issues and pull requests about actual bugs ux: highlighting Issues relating to syntax highlighting
#5053 opened Nov 12, 2020 by nad icebox
@andreasabel
2
Add a command to bring a variable mentioned in a goal into scope scope Issues relating to scope checking ux: interaction Issues to do with interactive development (holes, case splitting, etc)
#4337 opened Dec 29, 2019 by gallais icebox
2
Not in scope error instead of missing type signature error regression in 2.5.4 Regression that first appeared in Agda 2.5.4 scope Issues relating to scope checking ux: error reporting Issues to do with how Agda reports errors
#4150 opened Oct 21, 2019 by andreasabel icebox
@andreasabel
2
Parse error when something is not imported names scope Issues relating to scope checking type: bug Issues and pull requests about actual bugs ux: case splitting Issues relating to the case split ("C-c C-c") command ux: error reporting Issues to do with how Agda reports errors ux: printing Issues relating to how terms are printed for display
#4037 opened Aug 27, 2019 by Boarders icebox
3
Scope checker (?) superlinear performance performance Slow type checking, interaction, compilation or execution of Agda programs scope Issues relating to scope checking
#3997 opened Aug 16, 2019 by andreasabel icebox
@andreasabel
1
where module should be in scope in rhs of clause record expression Issues concerning record{...} expressions (record literals and record updates) records Record declarations, literals, constructors and updates scope Issues relating to scope checking type: enhancement Issues and pull requests about possible improvements where Problems with where clauses
#3823 opened May 30, 2019 by andreasabel icebox
@andreasabel
3
Allow declarations in inner scopes to shadow declarations in outer scopes language change Changes to the language which can be observed by Agda's userbase scope Issues relating to scope checking shadowing Problems caused by re-using names in the surface syntax ux: warnings Issues relating to the reporting of warnings
#3801 opened May 23, 2019 by andreasabel later
1
@andreasabel
6
Misleading error messages in mutual definitions. copatterns Definitions by copattern matching: projections on the LHS mutual parser Problems with the parser's implementation (rather than with decisions about syntax) scope Issues relating to scope checking
#3499 opened Jan 13, 2019 by semenov-vladyslav icebox
3
Discussion: make variables generalised in the type in scope for the clauses? generalize Related to generalisable variables scope Issues relating to scope checking type: discussion Discussions about Agda's design and implementation type: enhancement Issues and pull requests about possible improvements
#3447 opened Dec 11, 2018 by gallais icebox
4
"modules are not allowed in mutual block", but new-style implicit mutuals accept them modules Issues relating to the module system mutual scope Issues relating to scope checking type: discussion Discussions about Agda's design and implementation
#3246 opened Sep 27, 2018 by andreasabel icebox
@andreasabel
4
Printer prefers (longer) qualified over (shorter) unqualified name import Issues to do with importing modules modules Issues relating to the module system scope Issues relating to scope checking type: enhancement Issues and pull requests about possible improvements ux: printing Issues relating to how terms are printed for display
#3240 opened Sep 25, 2018 by andreasabel icebox
1
Case-split on a datatype defined in a parametrised module produces needlessly-prefixed patterns priority: high scope Issues relating to scope checking type: bug Issues and pull requests about actual bugs 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
#3209 opened Sep 3, 2018 by gallais 2.8.0
11
Pragmas and scopes pragma scope Issues relating to scope checking status: info-needed More information is needed from the bug reporter to confirm the issue.
#3077 opened May 23, 2018 by nad icebox
2
Suggest replacements for various unicode characters scope Issues relating to scope checking type: enhancement Issues and pull requests about possible improvements ux: error reporting Issues to do with how Agda reports errors
#2898 opened Jan 12, 2018 by fredefox icebox
4
Case split with non-trivial RHS should either be disallowed or do the right thing scope Issues relating to scope checking type: bug Issues and pull requests about actual bugs 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)
#2800 opened Oct 11, 2017 by jespercockx icebox
5
Search the scope of imported libraries scope Issues relating to scope checking type: enhancement Issues and pull requests about possible improvements ux: error reporting Issues to do with how Agda reports errors ux: library management Issues relating to the library management system
#2701 opened Aug 17, 2017 by andreasabel
1 of 5 tasks
icebox
4
ProTip! Find all open issues with in progress development work with linked:pr.