Editor Support - idris-lang/Idris2 GitHub 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 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.
From a term, jump to the file where it is defined
From a pattern variable, split it into its constructors and generate a suitable right-hand-side
From a term, get its type.
From a term get its documentation from its doc-comment
From a term that is publicly exported, get its implementation.
Suggest valid terms while typing
From a hole, generate a term that fits the type automatically. Allow to cycle through multiple candidates.
From a type signature, generate a skeleton definition. From an interface declaration, generate the list of required methods.
From anywhere in the program, move the cursor to the next hole that needs to be completed.
Avoid compiler errors while compiling code with multiple identical hole names, as per #640.
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 through the imported modules and find all the functions that implement a given type signature.
Code shown by the compiler is optionally coloured to facilitate readability.
Read-Eval-Print-Loop, a prompt with which to interact with the current file.
Based on the type signature, if the function is trivial, generate its body. (Particularly useful when implementing simple helper functions).