agda-mode icon indicating copy to clipboard operation
agda-mode copied to clipboard

Go to definition for mixfix operators without underscore fails

Open pnlph opened this issue 4 years ago • 1 comments

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.

pnlph avatar May 16 '20 08:05 pnlph

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.

banacorn avatar May 20 '20 07:05 banacorn