107 lines
5.5 KiB
Org Mode
107 lines
5.5 KiB
Org Mode
#+TITLE: Idris layer
|
|
|
|
[[file:img/idris.png]]
|
|
|
|
* Table of Contents :TOC_4_gh:noexport:
|
|
- [[#description][Description]]
|
|
- [[#install][Install]]
|
|
- [[#layer][Layer]]
|
|
- [[#idris][Idris]]
|
|
- [[#key-bindings][Key bindings]]
|
|
- [[#shorthands][Shorthands]]
|
|
- [[#interactive-editing][Interactive editing]]
|
|
- [[#documentation][Documentation]]
|
|
- [[#repl][REPL]]
|
|
- [[#active-term-manipulations][Active term manipulations]]
|
|
- [[#build-system][Build system]]
|
|
|
|
* Description
|
|
This layer adds support for the [[http://www.idris-lang.org/][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=:
|
|
|
|
#+BEGIN_SRC sh
|
|
cabal install idris
|
|
#+END_SRC
|
|
|
|
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 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. |
|
|
|
|
** 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. |
|
|
|
|
** 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. |
|
|
|
|
** 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 |
|
|
|
|
** 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. |
|
|
|
|
** 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~.
|