mirror of
https://github.com/SpaceVim/SpaceVim.git
synced 2025-01-24 02:10:05 +08:00
72 lines
2.1 KiB
Markdown
72 lines
2.1 KiB
Markdown
|
---
|
||
|
|
title: "SpaceVim lang#idris layer"
|
||
|
|
description: "This layer is for idris development, provide syntax checking, code runner and repl support for idris file."
|
||
|
|
image: https://user-images.githubusercontent.com/13142418/65492491-9dece000-dee3-11e9-8eda-7d41a6c1ee79.png
|
||
|
|
---
|
||
|
|
|
||
|
|
# [Available Layers](../../) >> lang#idris
|
||
|
|
|
||
|
|
<!-- vim-markdown-toc GFM -->
|
||
|
|
|
||
|
|
- [Description](#description)
|
||
|
|
- [Install](#install)
|
||
|
|
- [Features](#features)
|
||
|
|
- [Key bindings](#key-bindings)
|
||
|
|
- [Running current script](#running-current-script)
|
||
|
|
- [Inferior REPL process](#inferior-repl-process)
|
||
|
|
|
||
|
|
<!-- vim-markdown-toc -->
|
||
|
|
|
||
|
|
## Description
|
||
|
|
|
||
|
|
This layer is for idris development, which is based on [wsdjeg/vim-idris](https://github.com/wsdjeg/vim-idris).
|
||
|
|
|
||
|
|
## Install
|
||
|
|
|
||
|
|
To use this configuration layer, update custom configuration file with:
|
||
|
|
|
||
|
|
```toml
|
||
|
|
[[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 |
|