c893383fe4
- CSS links - GIFS in published version - Unify layer doc titles - Change emoji layer emojis to an image
108 lines
5.3 KiB
Org Mode
108 lines
5.3 KiB
Org Mode
#+TITLE: Idris layer
|
|
#+HTML_HEAD_EXTRA: <link rel="stylesheet" type="text/css" href="../../../css/readtheorg.css" />
|
|
|
|
[[file:img/idris.png]]
|
|
|
|
* Table of Contents :TOC_4_org: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 layer, add it to your =~/.spacemacs=
|
|
|
|
#+BEGIN_SRC elisp
|
|
(setq-default dotspacemacs-configuration-layers '(idris))
|
|
#+END_SRC
|
|
|
|
** 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. |
|
|
| ~SPC m d~ | Create an initial pattern match clause for a type declaration. |
|
|
| ~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. |
|
|
| ~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~.
|