herminie

Does the issue #agda/agda#4507 help?

Would this be available as a keybinding? Maybe it is also an option not having `QuickLaTeX` as a setting, because otherwise to scope check and then load the file, one...

If I understand right, the protocol itself does not provide the basis to build a full implementation of a language server for Agda. I see that it is possible to...

I am actually very happy with the explicited list of openings. It gives a good overview on how the definition/module is linked to the structure of the library in use....

Yes, makes sense. As a use case for its utility, I get the following when getting the scope info of `Universes` within the repository https://github.com/martinescardo/HoTT-UF-Agda-Lecture-Notes ``` Scope info Universe is...

Yes, this is a good idea. Can you post here such a list and we upload a first version?

> In cases where two distinct expressions are printed in the same way I think it makes sense to find some way to explain how they differ. I agree. Don't...

I could work on this, any hint on how to start?

Why not assigning numbered ids to every identifier, just like it is done with the identifier of the main module and the unnamed module? ```html _ ```

There is already a [pygments class](https://github.com/mhaberler/pygments/blob/master/pygments/lexers/haskell.py), but also for Idris and other haskell-related languages. Is this helping for having a new lexer or it must be built from scratch? ```...