Idris layer

Table of ContentsClose

1. Description
2. Install
- 2.1. Layer
- 2.2. Idris
3. Key bindings

1 Description

This layer adds support for the Idris language.

2 Install

2.1 Layer

To use this configuration layer, add it to your ~/.spacemacs. You will need to add idris to the existing dotspacemacs-configuration-layers list in this file.

2.2 Idris

Idris can be installed using Haskell's cabal:

cabal install idris

Binaries are also available for some platforms at http://www.idris-lang.org/download/

3 Key bindings

3.1 Shorthands

Several (but not all) of the evil-leader shorthands that idris-mode provides are reproduced under the local leader.

Key Binding	Description
`SPC m c`	Case split the pattern variable under point, or make it into a case expression.
`SPC m d`	Create an initial pattern match clause for a type declaration.
`SPC m l`	Extract lemma from hole
`SPC m p`	Attempt to solve a metavariable automatically.
`SPC m r`	Load current buffer into Idris.
`SPC m t`	Get the type for the identifier under point.
`SPC m w`	Add a with block for the pattern-match clause under point.

3.2 Interactive editing

Key Binding	Description
`SPC m i a`	Attempt to solve a metavariable automatically.
`SPC m i c`	Case split the pattern variable under point, or make it into a case expression.
`SPC m i e`	Extract a metavariable or provisional definition name to an explicit top level definition.
`SPC m i m`	Add missing pattern-match cases to an existing definition.
`SPC m i r`	Refine by name, without recursive proof search.
`SPC m i s`	Create an initial pattern match clause for a type declaration.
`SPC m i w`	Add a with block for the pattern-match clause under point.

3.3 Documentation

Key Binding	Description
`SPC m h a`	Search the documentation for a string.
`SPC m h d`	Search the documentation for the name under point.
`SPC m h s`	Search the documentation regarding a particular type.
`SPC m h t`	Get the type for the identifier under point.

3.4 REPL

Key Binding	Description
`SPC m s b`	Load the current buffer into Idris.
`SPC m s B`	Load the current buffer into Idris and switch to REPL in insert state
`SPC m s i`	Start Idris inferior process
`SPC m s n`	Extend the region to be loaded one line at a time.
`SPC m s N`	Extend the region to be loaded one line at a time and switch to REPL in insert state
`SPC m s p`	Contract the region to be loaded one line at a time
`SPC m s P`	Contract the region to be loaded one line at a time and switch to REPL in insert state
`SPC m s s`	Switch to REPL buffer
`SPC m s q`	Quit the Idris process

3.5 Active term manipulations

Key Binding	Description
`SPC m m c`	Show the core language for the term at point.
`SPC m m i`	Show implicits for the term at point.
`SPC m m h`	Hide implicits for the term at point.
`SPC m m n`	Normalize the term at point.

3.6 Build system

Key Binding	Description
`SPC m b c`	Build the package.
`SPC m b C`	Clean the package, removing `.ibc` files
`SPC m b i`	Install the package to the user's repository, building first if necessary.
`SPC m b p`	Open package file.

When inside a package file, you can insert a field with SPC m f.