Idris for Visual Studio Code

Implemented features

command screenshot	command name
Typechecking	idris.typecheck
Show the types of a variable	idris.type-of
Show the doc for a variable	idris.docs-for
Show the doc for a definition	idris.print-definition
Show holes	idris.show-holes
Add clause	idris.add-clause
Add proof clause	idris.add-proof-clause
Split case	idris.case-split
Search proof	idris.proof-search
Make with	idris.make-with
Make case	idris.make-case
Make lemma	idris.make-lemma
Apropos	idris.apropos
Eval selected code	idris.eval-selection
Start / Refresh REPL	idris.start-refresh-repl
Send selected code to REPL	idris.send-selection-repl
Cleanup Idris binary files	idris.cleanup-ibc

Heads up: All the command 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
• Project Scaffolding

Installation

1. Within Visual Studio Code, open the command palette (Ctrl-Shift-P / Cmd-Shift-P).
2. Select Install Extension and search for Idris or run ext install Idris.
3. Download Idris and make sure the idris executable is on your PATH.
4. Run cabal install idringen and make sure the idrin executable is on your PATH.

Contributing

Check out CONTRIBUTING.md.

Options

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": true        // Show warning when a function is partial.
}

Acknowledgements

• The internal design is initially inspired by atom-language-idris.

Thanks

• Belleve Invis @be5invis (The maintainer of the syntax files)

License

BSD 3-Clause, the same as Idris.