This layer adds support for the Idris2 language to Spacemacs, and is completely based on the Idris layer.
- wrapper around the official idris2-mode
- follows the same command list as Idris Spacemacs layer
- extends with new Idris2 features
- Add this layer to the private layers
git clone --recursive [email protected]:cyberglot/idris2-spacemacs.git .emacs.d/private/idris2
- Activate the layer in your
~/.spacemacs
dotspacemacs-configuration-layers '(... idris2)
Or you can add it in dotspacemacs-additional-packages:
(idris2-mode :location (recipe :fetcher github :repo "cyberglot/idris2-spacemacs")
Idris2 can be installed with binaries available for some platforms at
https://www.idris-lang.org/pages/download.html.
Several (but not all) of the evil-leader shorthands that idris2-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. |
SPC m n | Next error. |
SPC m p | Previous error. |
| 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 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. |
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. |
SPC m h j | Jump to definition. |
SPC m h w | Jump to definition (New window). |
| 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 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 and switch to REPL in insert state |
SPC m s s | Switch to REPL buffer |
| 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.