Skip to content

cyberglot/idris2-spacemacs

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

15 Commits
 
 
 
 
 
 

Repository files navigation

Idris2 layer

Table of Contents

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 bindingDescription
SPC m cCase split the pattern variable under point, or make it into a case expression.
SPC m dCreate an initial pattern match clause for a type declaration.
SPC m lExtract lemma from hole
SPC m pAttempt to solve a metavariable automatically.
SPC m rLoad current buffer into Idris.
SPC m tGet the type for the identifier under point.
SPC m wAdd a with block for the pattern-match clause under point.
SPC m nNext error.
SPC m pPrevious error.

Interactive editing

Key bindingDescription
SPC m i aAttempt to solve a metavariable automatically.
SPC m i cCase split the pattern variable under point, or make it into a case expression.
SPC m i eExtract a metavariable or provisional definition name to an explicit top level definition.
SPC m i sCreate an initial pattern match clause for a type declaration.
SPC m i wAdd a with block for the pattern-match clause under point.

Documentation

Key bindingDescription
SPC m h dSearch the documentation for the name under point.
SPC m h sSearch the documentation regarding a particular type.
SPC m h tGet the type for the identifier under point.
SPC m h jJump to definition.
SPC m h wJump to definition (New window).

REPL

Key bindingDescription
SPC m s bLoad the current buffer into Idris.
SPC m s BLoad the current buffer into Idris and switch to REPL in insert state
SPC m s nExtend the region to be loaded one line at a time.
SPC m s NExtend the region to be loaded one line at a time and switch to REPL in insert state
SPC m s PContract the region to be loaded one line at a time and switch to REPL in insert state
SPC m s sSwitch to REPL buffer

Build system

Key bindingDescription
SPC m b cBuild the package.
SPC m b CClean the package, removing .ibc files.
SPC m b iInstall the package to the user’s repository, building first if necessary.
SPC m b pOpen package file.

When inside a package file, you can insert a field with SPC m f.

About

It may work, use at your own discretion.

Topics

Resources

License

Stars

Watchers

Forks