Heads up: All the commands above can also be triggered in the right-click menu
- iPKG
- Auto-completion
- Show type definition on hover
- Type checking on saving file
- Go to Definition and Peek Definition
- Go to Symbol (Outline symbols in currently opend file)
- Search Symbol (Outline symbols in currently opend project)
- Find all references
- Rename symbol
- Change all occurrences
- Latex snippets
- Literate Idris
- Document highlights
- Parameter hints
- Within Visual Studio Code, open the command palette (Ctrl-Shift-P / Cmd-Shift-P).
- Select
Install Extensionand search for Idris or runext install Idris. - Download Idris and make sure the idris executable is on your
PATH. - Run
cabal install idringenand make sure the idrin executable is on yourPATH.
Check out CONTRIBUTING.md.
The following Visual Studio Code settings along with their default values that are available for the Idris extension. If you want to change any of these, you can do so in user preferences (cmd+,) or workspace settings (.vscode/settings.json). You don't have to copy these if you don't intend to change them.
{
"idris.executablePath": "idris", // The full path to the idris executable.
"idris.hoverMode": "fallback", // Controls the hover behavior. 'info' will display Idris documentation, 'type' will display Idris type, 'fallback' will try 'info' first and fallback to 'type' if we can not get the documentation, and 'none' will disable hover tooltips.
"idris.suggestMode": "allWords" // Controls the auto-completion behavior. 'allWords' will always include all words from the currently opened documentation, 'replCompletion' will get suggestions from Idris REPL process.
"idris.warnPartial": false // Show warning when a function is partial.
"idris.showOutputWhenTypechecking": false //Show output channel when typechecking finished.
"idris.numbersOfContinuousTypechecking": 10 //Kill Idris process every N times of continuous typechecking to avoid memory leaking.
}- The internal design is initially inspired by atom-language-idris.
- Belleve Invis @be5invis (The maintainer of the syntax files)
BSD 3-Clause, the same as Idris.