Idris layer

Table of ContentsClose

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

1. Description

This layer adds support for the Idris language to Spacemacs.

1.1. Features:

Syntax highlighting
Syntax checking via flycheck
Integration of the Idris REPL
Integration of the Idris build system

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 https://www.idris-lang.org/pages/download.html

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.