Ting-gian LUA

Thanks!

+1

I run this instead. ``` ghci -package-db=cabal-dev/packages-7.6.3.conf ```

Hmm, I don't know. First I tried `agda --latex somefile.lagda` in the terminal (without the ` --only-scope-checking` flag). It said it typed checked the file, but then in the next...

Thanks, found it! https://github.com/agda/agda/blob/8c30a29fd73f4b19f2866f31712be102929dbfe5/src/full/Agda/Interaction/Base.hs#L407-L413 So it turned out to be a backend itself, and it's not available from the Atom's agda-mode yet. It shouldn't be difficult to add a new...

Yes that would be possible!

Those command language services are a part of what is called the [Language Server Protocol](https://microsoft.github.io/language-server-protocol/). I've investigated LSP quite a bit and even tried to implement a language server for...

I'm not sure, even if the extension is added, it'll still be quite an effort.

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.

I'm picturing a dropdown list of links (like in fuzzy search shift-cmd-p) when there are multiple sources of definition. I've seen other languages doing the same thing. Would that be...