You are viewing the documentation for the develop branch. The documentation for the release version is here .

Table of Contents

Idris layer

Table of ContentsClose

idris.png

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.

Author: root

Created: 2021-09-29 Wed 20:45

Validate