A syntax highlighting extension for the Agda programming language.
Features
Highlight Agda syntax in Agda, Literate Agda (LaTeX), and Markdown files.
Add keybindings for using agda-mode with Literate Agda and Markdown files.
Setup
The extension works straight out of the box. However, if you are using this extension together with agda-mode, there are some settings you may want to change for a better user experience.
You may want to
set the option editor.autoClosingPairs to "never" for files used with agda-mode as this function interferes with Agda's input-mode.
If you are writing literate Agda LaTeX code, rebind the input-mode key (agda-mode.input-symbol[Activate]) from backslash (\) to some other key.
If you are using literate Agda Markdown files, add the following file association to your settings.json: