Feedbacks, issues, and PRs all welcome!
- Make sure that you have agda properly installed (to check this in your terminal, type
agdaand see if it's on your machine). - Open an Agda file and you should be able to load it by typing C-c C-l.
The language server is still under heavy development, but if you want to try it out, please follow these instructions. You should see "LSP" instead of "Emacs" on the top right of the panel if it worked.
- C-c stands for "press Ctrl and c at the same time"
- When it comes to combos like C-c C-l, you can often slur them into "hold Ctrl while pressing c and then l"
Commands working with types (marked with the 🎚 emoji below) can have different levels of normalization. However, due to some technical limitations, we cannot prefix commands with C-u or C-u C-u like in Emacs. Instead, we replace the C-u C-c prefix with C-u and the C-u C-u C-c prefix with C-y.
Take infer type for example:
| Level of normalization | Keymap in VS Code | Keymap in Emacs |
|---|---|---|
| "simplified" (default) | C-c C-d | C-c C-d |
| "instantiated" (without further normalisation) | C-u C-d | C-u C-c C-d |
| "normalized" (fully normalized) | C-y C-d | C-u C-u C-c C-d |
| Command | Keymap |
|---|---|
| load | C-c C-l |
| compile | C-x C-c |
| quit | C-c C-q |
| quit and restart | C-x C-r |
| toggle display of hidden arguments | C-x C-h |
| show constraints | C-c C-= |
| solve constraints 🎚 | C-c C-s |
| show all goals | C-c C-? |
| move to next goal (forward) | C-c C-f |
| move to previous goal (backwards) | C-c C-b |
| infer type 🎚 | C-c C-d |
| module contents 🎚 | C-c C-o |
| search definitions in scope 🎚 | C-c C-z |
| compute normal form (default compute) | C-c C-n |
| compute normal form (ignore abstract) | C-u C-n |
| compute normal form (use show instance) | C-y C-n |
| switch to a different Agda version | C-x C-s |
| Command | Keymap |
|---|---|
| give (fill goal) | C-c C-SPC |
| refine | C-c C-r |
| elaborate and give 🎚 | C-c C-m |
| auto | C-c C-a |
| case split | C-y C-c |
| compute helper function type and copy 🎚 | C-y C-h |
| goal type 🎚 | C-c C-t |
| context (environment) 🎚 | C-c C-e |
| infer type 🎚 | C-c C-d |
| goal type and context 🎚 | C-c C-, |
| goal type, context and inferred term 🎚 | C-c C-. |
| goal type, context and checked term 🎚 | C-c C-; |
| module contents 🎚 | C-c C-o |
| compute normal form (default compute) | C-c C-n |
| compute normal form (ignore abstract) | C-u C-n |
| compute normal form (use show instance) | C-y C-n |
| why in scope | C-c C-w |
| Command | Keymap |
|---|---|
| abort a command | C-x C-a |
| remove goals and highlighting | C-x C-d |
| comment/uncomment rest of buffer |
Pretty much the same like on Emacs. Press backslash "\" and you should see a keyboard popping up in the panel, with key suggestions and symbol candidates. Use arrow keys to explore and navigate between the candidates (if there's any).
Unicode input also works in the input prompt, though it's a bit less powerful.
Please open the "Keyboard Shortcuts" tool (C-k + C-s) and see if any other extensions are fighting for the same key combinations.
Give (C-c C-SPC) would trigger "Spotlight" (C-SPC) on Mac. Please consider using Refine (C-c C-r) instead.
See CONTRIBUTING.md