Skip to content
Jan de Muijnck-Hughes edited this page Oct 31, 2022 · 5 revisions

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
  • Case split
  • Get type
  • Get documentation
  • Get definition
  • Autocomplete
  • Proof search
  • Skeleton definition
  • Jump to next hole
  • Hole list
  • Suggest hole names
  • Compiler history
  • Search from signature
  • Coloured code output
  • A REPL
  • Generate definition
  • 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).