docs/layers/lang/idris.md
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 |