-
Notifications
You must be signed in to change notification settings - Fork 339
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.
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
Tactic command runs forever #5283
Labels
reflection
Elaborator reflection, macros, tactic arguments
regression in 2.6.1
Regression that first appeared in Agda 2.6.1
tactic
tactic annotations
Milestone
Comments
MWE: open import Agda.Builtin.Reflection
A : Set
A = tactic ? This fails in 2.6.0 with unsolved constraints, starting with 2.6.1 it loops. |
Turns out that the scope checker accepts |
andreasabel
added a commit
that referenced
this issue
Aug 19, 2021
'tactic' can only appear in attributes, it has been added to Abstract.Syntax on error.
andreasabel
added a commit
that referenced
this issue
Aug 19, 2021
This is an unused constructor that only causes confusion.
andreasabel
added a commit
that referenced
this issue
Aug 19, 2021
'tactic' can only appear in attributes, it has been added to Abstract.Syntax on error.
andreasabel
added a commit
that referenced
this issue
Aug 19, 2021
This is an unused constructor that only causes confusion.
andreasabel
added a commit
that referenced
this issue
Nov 17, 2021
'tactic' can only appear in attributes, it has been added to Abstract.Syntax on error.
andreasabel
added a commit
that referenced
this issue
Nov 17, 2021
This is an unused constructor that only causes confusion.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Labels
reflection
Elaborator reflection, macros, tactic arguments
regression in 2.6.1
Regression that first appeared in Agda 2.6.1
tactic
tactic annotations
When I try to compile this program, it never finishes:
The text was updated successfully, but these errors were encountered: