mirror of
https://github.com/SpaceVim/SpaceVim.git
synced 2025-01-23 22:20:06 +08:00
2.1 KiB
2.1 KiB
| title | description | image |
|---|---|---|
| SpaceVim lang#idris layer | This layer is for idris development, provide syntax checking, code runner and repl support for idris file. | https://user-images.githubusercontent.com/13142418/65492491-9dece000-dee3-11e9-8eda-7d41a6c1ee79.png |
Available Layers >> lang#idris
Description
This layer is for idris development, which is based on wsdjeg/vim-idris.
Install
To use this configuration layer, update custom configuration file with:
[[layers]]
name = "lang#idris"
Features
- repl support
- code runner
- show symbol doc
- show symbol type
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 running a idris file, you can press SPC l r to run current file without loss 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 |