Skip to content
This repository has been archived by the owner on Feb 26, 2021. It is now read-only.

Go to definition for mixfix operators without underscore fails #125

Open
pnlph opened this issue May 16, 2020 · 1 comment
Open

Go to definition for mixfix operators without underscore fails #125

pnlph opened this issue May 16, 2020 · 1 comment
Labels

Comments

@pnlph
Copy link

pnlph commented May 16, 2020

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.

@banacorn
Copy link
Owner

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 banacorn added the bug label May 20, 2020
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Labels
Projects
None yet
Development

No branches or pull requests

2 participants