Idris mode for vim
I recommend using Pathogen for installation. Simply clone this repo into your
~/.vim/bundledirectory and you are ready to go.
cd ~/.vim/bundle git clone https://github.com/idris-hackers/idris-vim.git
Copy content into your
Be sure that the following lines are in your
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.
Idris mode for vim offers interactive editing capabilities, the following commands are supported.
dCreate an initial clause for a type declaration.
bSame as \d but for an initial typeclass method impl.
mdSame as \d but for a proof clause
wadd with clause
madd missing clause
oobvious proof search
iopen idris response window
To configure indentation in
idris-vimyou 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 >>>>x
let g:idris_indent_where = 6
where f : Int -> Int >>>>>>f x = x
let g:idris_indent_do = 3
do x >>y
let g:idris_indent_rewrite = 8
rewrite prf in expr >>>>>>>>x
Concealing with unicode characters is off by default, but
let g:idris_conceal = 1turns it on.
If you simply must use tab characters, and would prefer that the ftplugin not set expandtab add
let g:idris_allow_tabchar = 1.