Skip to content

Files

Latest commit

b252d25 · Apr 2, 2017

History

History
This branch is 432 commits ahead of, 6193 commits behind develop.

idris

Folders and files

NameName
Last commit message
Last commit date

parent directory

..
Sep 22, 2015
Jul 2, 2016
Jul 2, 2016
Apr 2, 2017

Idris layer

img/idris.png

Table of Contents

Description

This layer adds support for the Idris language.

Install

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.

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/

Key bindings

Shorthands

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

Key BindingDescription
SPC m cCase split the pattern variable under point, or make it into a case expression.
SPC m dCreate an initial pattern match clause for a type declaration.
SPC m lExtract lemma from hole
SPC m pAttempt to solve a metavariable automatically.
SPC m rLoad current buffer into Idris.
SPC m tGet the type for the identifier under point.
SPC m wAdd a with block for the pattern-match clause under point.

Interactive editing

Key BindingDescription
SPC m i aAttempt to solve a metavariable automatically.
SPC m i cCase split the pattern variable under point, or make it into a case expression.
SPC m i eExtract a metavariable or provisional definition name to an explicit top level definition.
SPC m i mAdd missing pattern-match cases to an existing definition.
SPC m i rRefine by name, without recursive proof search.
SPC m i sCreate an initial pattern match clause for a type declaration.
SPC m i wAdd a with block for the pattern-match clause under point.

Documentation

Key BindingDescription
SPC m h aSearch the documentation for a string.
SPC m h dSearch the documentation for the name under point.
SPC m h sSearch the documentation regarding a particular type.
SPC m h tGet the type for the identifier under point.

REPL

Key BindingDescription
SPC m s bLoad the current buffer into Idris.
SPC m s BLoad the current buffer into Idris and switch to REPL in insert state
SPC m s iStart Idris inferior process
SPC m s nExtend the region to be loaded one line at a time.
SPC m s NExtend the region to be loaded one line at a time and switch to REPL in insert state
SPC m s pContract the region to be loaded one line at a time
SPC m s PContract the region to be loaded one line at a time and switch to REPL in insert state
SPC m s sSwitch to REPL buffer
SPC m s qQuit the Idris process

Active term manipulations

Key BindingDescription
SPC m m cShow the core language for the term at point.
SPC m m iShow implicits for the term at point.
SPC m m hHide implicits for the term at point.
SPC m m nNormalize the term at point.

Build system

Key BindingDescription
SPC m b cBuild the package.
SPC m b CClean the package, removing .ibc files
SPC m b iInstall the package to the user’s repository, building first if necessary.
SPC m b pOpen package file.

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