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/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.

Author: Travis CI User

Created: 2019-01-22 Tue 20:42

Validate