SpaceVim
A modular Vim/Neovim configuration
Home | About | Quick start guide | Documentation | Development | Community | Sponsors | 中文
This layer is for idris development, which is based on wsdjeg/vim-idris.
To use this configuration layer, update your custom configuration file with:
[[layers]]
name = "lang#idris"
| 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 |
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.
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