Go to file
rhiannon morris 8d61704813 change highlight categories 2023-11-05 12:10:48 +01:00
after Initial version 2020-02-22 20:32:56 +00:00
doc Initial version 2020-02-22 20:32:56 +00:00
ftdetect Further "Idris" -> "Idris 2" renamings were done 2020-05-19 18:32:37 +03:00
ftplugin add type search on \s (since proof search is ALSO \o) 2023-05-28 14:45:18 +02:00
indent remove } from indk 2021-12-28 09:56:16 +01:00
syntax change highlight categories 2023-11-05 12:10:48 +01:00
syntax_checkers/idris2 Further "Idris" -> "Idris 2" renamings were done 2020-05-19 18:32:37 +03:00
README.md add \T to readme 2021-12-28 09:58:08 +01:00


Idris 2 mode for vim

This is an Idris2 mode for vim which features interactive editing, syntax highlighting, indentation and optional syntax checking via Syntastic. If you need a REPL I recommend using Vimshell. It is mostly cloned from the original idris-mode. Unlike the Idris 1 mode, there is no need to have an Idris REPL running - it invokes Idris 2 directly.

If there is a .ipkg file in any of the parent directories, the mode will use that as the root of the source tree, and process any options declared in it (for example, to load packages).

Not all of the commands work yet. Note that the keyboard shortcuts have been updated since Idris 1 to be consistent with the Atom mode (e.g. <LocalLeader>a to add definition, rather than <LocalLeader>d) although the old shortcuts still work.



I recommend using Pathogen for installation. Simply clone this repo into your ~/.vim/bundle directory and you are ready to go.

cd ~/.vim/bundle
git clone https://github.com/edwinb/idris2-vim.git

Manual Installation

Copy content into your ~/.vim directory.

Be sure that the following lines are in your .vimrc

syntax on
filetype on
filetype plugin indent on


Apart from syntax highlighting, indentation, and unicode character concealing, idris-vim offers some neat interactive editing features. For more information on how to use it, read this blog article by Edwin Brady on Interactive Idris editing with vim.

Interactive Editing Commands

Idris2 mode for vim offers interactive editing capabilities, the following commands are supported.

<LocalLeader>r reload file

<LocalLeader>t show type

<LocalLeader>T show type with all implicits

<LocalLeader>a Create an initial clause for a type declaration.

<LocalLeader>c case split

<LocalLeader>mc make case

<LocalLeader>w add with clause

<LocalLeader>e evaluate expression

<LocalLeader>l make lemma

<LocalLeader>m add missing clause

<LocalLeader>f refine item

<LocalLeader>o obvious proof search

<LocalLeader>s proof search

<LocalLeader>i open idris response window

<LocalLeader>d show documentation



To configure indentation in idris-vim you can use the following variables:

  • let g:idris_indent_if = 3

      if bool
      >>>then ...
      >>>else ...
  • let g:idris_indent_case = 5

      case xs of
      >>>>>[]      => ...
      >>>>>(y::ys) => ...
  • let g:idris_indent_let = 4

      let x = 0 in
  • let g:idris_indent_where = 6

      where f : Int -> Int
      >>>>>>f x = x
  • let g:idris_indent_do = 3

      do x <- a
      >>>y <- b
  • let g:idris_indent_rewrite = 8

      rewrite prf in expr


Concealing with unicode characters is off by default, but let g:idris_conceal = 1 turns it on.

Tab Characters

If you simply must use tab characters, and would prefer that the ftplugin not set expandtab add let g:idris_allow_tabchar = 1.