Idris2 layer

Table of Contents

• Description
• Features
• Install
  • Layer
  • Idris2
• Key bindings
  • Shorthands
• Interactive editing
• Documentation
• REPL
• Build system

Description

This layer adds support for the Idris2 language to Spacemacs, and is completely based on the Idris layer.

Features

• wrapper around the official idris2-mode
• follows the same command list as Idris Spacemacs layer
• extends with new Idris2 features

Install

Layer

1. Add this layer to the private layers

git clone --recursive [email protected]:cyberglot/idris2-spacemacs.git .emacs.d/private/idris2

1. 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

Idris2 can be installed with binaries available for some platforms at https://www.idris-lang.org/pages/download.html.

Key bindings

Shorthands

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.

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 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 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).

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 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

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.