Check out FEATURES.md to see screenshots for implemented features.
command | shortcut |
---|---|
Typechecking | shift + cmd/ctrl + alt + t |
Show the types of a variable | shift + cmd/ctrl + alt + o |
Show the doc for a variable | shift + cmd/ctrl + alt + d |
Show the doc for a definition | shift + cmd/ctrl + alt + f |
Show holes | shift + cmd/ctrl + alt + h |
Add clause | shift + cmd/ctrl + alt + a |
Split case | shift + cmd/ctrl + alt + c |
Search proof | shift + cmd/ctrl + alt + s |
Make with | shift + cmd/ctrl + alt + w |
Make case | shift + cmd/ctrl + alt + m |
Make lemma | shift + cmd/ctrl + alt + l |
Apropos | shift + cmd/ctrl + alt + k |
Eval selected code | shift + cmd/ctrl + alt + e |
Start / Refresh REPL | shift + cmd/ctrl + alt + r |
Send selected code to REPL | shift + cmd/ctrl + alt + x |
Cleanup Idris binary files | shift + cmd/ctrl + alt + u |
Heads up: All the command above can also be triggered in the right-click menu
- ipkg highlighting
- Auto-completion
- Show type definition on hover
- Type checking on saving file
Go to Definition
andPeek Definition
- Within Visual Studio Code, open the command palette (Ctrl-Shift-P / Cmd-Shift-P).
- Select
Install Extension
and search for 'Idris' or runext install Idris
. - Download Idris and make sure the
idris
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.
}
- Internal design is inspired by atom-language-idris.
BSD 3-Clause, the same as Idris.