agda-mode
agda-mode copied to clipboard
Go to definition for mixfix operators without underscore fails
Related with #119 and #122.
I noticed that when I try to get the Scope Info
of the constructor _,_
, the agda-mode
replies that , is not in scope.
Example:
pattern []' = (true , refl)
It works only when the operator appears in the code with the underscores:
pattern []' = (_,_ true refl)
In more complex fragments of code, this change is sometimes not so easy to perform.
Thanks for reporting this, I'm currently porting agda-mode to both Atom and VSCode. I'll see if this can get fix on the new rewrite.