The Idris editor experience - idris-lang/Idris2 Wiki

As a dependently typed language, the Idris compiler has access to a lot of information from the programs it typechecks. One use for this information is to streamline the development process by providing a user experience akin to a discussion with the compiler rather than a fight. This page aims to list and record which features are supported by which editors as well as links to the tool to install the necessary plugins to use those editor features.

Features Idris2-LSP idris2-vim idris2-mode (Emacs)
Go to definition [x] [ ] [x]
Case split [x] [x] [x]
Get type [x] [x] [x]
Get documentation [x] [x] [ ]
Get definition [ ] [ ] [ ]
Autocomplete [ ] [ ] [ ]
Proof search [x] [x] [x]
Skeleton definition [x] [x] [x]
Jump to next hole [x] [ ] [ ]
Hole list [x] [ ] [x]
Suggest hole names [ ] [ ] [ ]
Compiler history [ ] [ ] [ ]
Search from signature [ ] [ ] [ ]
Coloured code output [x] [x] [x]
A REPL [ ] [x] [x]
Generate definition [x] [x] [x]

Go to definition

From a term, jump to the file where it is defined

Case split

From a pattern variable, split it into its constructors and generate a suitable right-hand-side

Get type

From a term, get its type.

Get documentation

From a term get its documentation from its doc-comment

Get definition

From a term that is publicly exported, get its implementation.

Autocomplete

Suggest valid terms while typing

Proof search

From a hole, generate a term that fits the type automatically. Allow to cycle through multiple candidates.

Skeleton definition

From a type signature, generate a skeleton definition. From an interface declaration, generate the list of required methods.

Jump to next hole

From anywhere in the program, move the cursor to the next hole that needs to be completed.

Suggest hole names

Avoid compiler errors while compiling code with multiple identical hole names, as per #640.

Compiler history

Allow to show the history of previous compiler messages. This is particularly useful when comparing type signatures, effects of rewrites or types of holes.

Search from signature

Search through the imported modules and find all the functions that implement a given type signature.

Coloured code output

Code shown by the compiler is optionally coloured to facilitate readability.

REPL

Read-Eval-Print-Loop, a prompt with which to interact with the current file.

Generate definition

Based on the type signature, if the function is trivial, generate its body. (Particularly useful when implementing simple helper functions).