Idris2

Table of Contents

Go to definition
Case split
Get type
Get documentation
Get definition
Autocomplete
Proof search
Skeleton definition
Jump to next hole
Suggest hole names
Compiler history
Search from signature
Coloured code output
REPL
Generate definition

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 lists which features are supported by which editors, and provides links to the tools necessary to use those editor features.

If you are running a Unix-based OS and want to use the Neovim editor, you can find an (opinionated) setup guide here.

Feature	Idris2-LSP	idris2-vim	idris2-mode (Emacs)	idris-mode (Emacs)
Go to definition	[x]	[ ]	[x]	[x]
Case split	[x]	[x]	[x]	[x]
Get type	[x]	[x]	[x]	[x]
Get documentation	[x]	[x]	[ ]	[ ]
Get definition	[ ]	[ ]	[ ]	[ ]
Autocomplete	[ ]	[ ]	[ ]	[ ]
Proof search	[x]	[x]	[x]	[x]
Skeleton definition	[x]	[x]	[x]	[x]
Jump to next hole	[x]	[ ]	[ ]	[ ]
Hole list	[x]	[ ]	[x]	[x]
Suggest hole names	[ ]	[ ]	[ ]	[ ]
Compiler history	[ ]	[ ]	[ ]	[ ]
Search from signature	[ ]	[ ]	[ ]	[ ]
Coloured code output	[x]	[x]	[x]	[x]
A REPL	[ ]	[x]	[x]	[x]
Generate definition	[x]	[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).