|
…
|
||
|---|---|---|
| .. | ||
| img | ||
| packages.el | ||
| README.md | ||
Idris contribution layer for Spacemacs
Table of Contents
Description
This layer adds support for the Idris language.
This layer is in construction, it needs your contributions and bug reports.
Install
Layer
To use this layer, add it to your ~/.spacemacs
(setq-default dotspacemacs-configuration-layers '(idris))
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
All Idris specific bindings are prefixed with the major-mode leader SPC m.
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 r | Load current buffer into Idris. SPC m t | Get the type for the identifier under point. SPC m d | Create an initial pattern match clause for a type declaration. SPC m c | Case split the pattern variable under point. SPC m w | Add a with block for the pattern-match clause under point. SPC m p | Attempt to solve a metavariable automatically.
Interactive editing
Interactive editing commands are prefixed by SPC m i.
Key Binding | Description
---------------------|------------------------------------------------------------ SPC m i s | Create an initial pattern match clause for a type declaration. SPC m i m | Add missing pattern-match cases to an existing definition. SPC m i a | Attempt to solve a metavariable automatically. SPC m i e | Extract a metavariable or provisional definition name to an explicit top level definition. SPC m i c | Case split the pattern variable under point. SPC m i w | Add a with block for the pattern-match clause under point. SPC m i r | Refine by name, without recursive proof search.
Documentation
Documentation commands are prefixed by SPC m h.
Key Binding | Description
---------------------|------------------------------------------------------------ SPC m h d | Search the documentation for the name under point. SPC m h a | Search the documentation for a string. SPC m h s | Search the documentation regarding a particular type. SPC m h t | Get the type for the identifier under point.
File loading
File loading commands are prefixed by SPC m l.
Key Binding | Description
---------------------|------------------------------------------------------------ SPC m l b | Load the current buffer into Idris. SPC m l n | Extend the region to be loaded, if such a region exists, one line at a time. SPC m l p | Contract the region to be loaded, if such a region exists, one line at a time. SPC m l N | Contract the region to be loaded, if such a region exists, one line at a time.
Active term manipulations
Active term manipulations are prefixed by SPC m m.
Key Binding | Description
---------------------|------------------------------------------------------------ SPC m m n | Normalize 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 c | Show the core language for the term at point.
Build system
Commands for ipkg are prefixed by SPC m b.
Key Binding | Description
---------------------|------------------------------------------------------------
SPC m b c | Clean the package, removing .ibc files.`
SPC m b b | Build the package.
SPC m b i | Install the package to the user's repository, building first if necessary.
When inside a package file, you can insert a field with SPC m f.
REPL
You can pop to the corresponding Idris REPL with SPC m s.