agda-mode-vscode

agda-mode-vscode copied to clipboard

When you ask for an inferred type via one of `Agda: Infer Type (simplified, normalised, instantiated)` the information is given to you almost instantly, I assume all it does is...

MathiasSven

This code seems to parse the version of Agda from the output of `agda -V`: https://github.com/banacorn/agda-mode-vscode/blob/905ec6189976b98f6806d73c735c9602c0f39bda/src/Connection/Emacs/Connection__Emacs.res#L35 Agda >= 2.6.4 should have a `--numeric-version` option. - https://github.com/agda/agda/pull/6522 This could be utilized...

andreasabel

I use the [latex-input](https://marketplace.visualstudio.com/items?itemName=yellpika.latex-input) plugin to provide access to unicode characters. I've grown used to this, which I use across all languages in VSCode, and so I'd like to keep...

MevenBertrand

Minimal reproducing example ```agda a = {! b\nc !} ``` Using `C-c C-n`, one gets

fredrik-bakke

Fails to connect to a Agda Language Server running on NixOS on WSL

1

I am on Windows 10 and I want to write some Agda code. The [HoTT Game](https://thehottgameguide.readthedocs.io/en/latest/index.html) [recommends](https://thehottgameguide.readthedocs.io/en/latest/getting-started/installation.html#id12) that I install NixOS on WSL2 and run Agda there. So I installed...

VladimirMarko

Hi sorry if this is a basic question. But when I try to normalize expression with C-c, C-n the text shows up but I can not type anything except for...

Maylibooyah69