A modular Vim/Neovim configuration

Home | About | Quick start guide | Documentation | Development | Community | Sponsors | 中文

Available Layers » lang#idris


This layer is for idris development, which is based on wsdjeg/vim-idris.


To use this configuration layer, update your custom configuration file with:

  name = "lang#idris"


Key bindings

Key Bindings Descriptions
SPC l a reload current file
SPC l w add with clause
SPC l t show type
SPC l p proof search
SPC l o obvious proof search
SPC l c case split
SPC l f refine item
SPC l l make lemma
SPC l m add missing
SPC l h show doc
SPC l e idris eval
SPC l i open response win

Running current script

To run an idris file, you can press SPC l r to run the current file without losing focus, and the result will be shown in a runner buffer.

Inferior REPL process

Start a idris --nobanner inferior REPL process with SPC l s i.

Send code to inferior process commands:

Key Bindings Descriptions
SPC l s b send buffer and keep code buffer focused
SPC l s l send line and keep code buffer focused
SPC l s s send selection text and keep code buffer focused

Powered by Jekyll