SpaceVim

A modular Vim/Neovim configuration


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


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 your custom configuration file with:

[[layers]]
  name = "lang#idris"

Features

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