ff8cd06046
- lists were not correctly indented sometimes - **note** and such things do not exist in org - Note and Important - Change Feature list to heading - Change TODOS to actual org TODOS - Add TOC to python layer - list indentation - some typos I could not leave unchanged - TODO formatting - List indentation - typos - wrong markup fix conversion issues |
||
|---|---|---|
| .. | ||
| extensions.el | ||
| README.org | ||
Agda contribution layer for Spacemacs
Table of Contents TOC@4
Description
This layer adds support for the Agda programming language.
Some features:
- Faces redefined to correctly play with themes.
- Spacemacs bindings to Agda's interactive tools.
This layer is in construction, it needs your contributions and bug reports.
Install
Layer
To use this contribution add it to your ~/.spacemacs
(setq-default dotspacemacs-configuration-layers '(agda))Agda
Quick instructions to install Agda assuming you have cabal installed:
cabal install alex happy "cpphs < 1.19" agda
Then check that agda is available on your PATH and seen by Emacs.
Key bindings
The key bindings of this layer don't follow the Spacemacs conventions, we opted to a simple transcription of stock Agda mode key bindings to Spacemacs leader key.
All Agda specific bindings are prefixed with the major-mode leader
SPC m.
| Key Binding | Description |
|---|---|
SPC m = |
Show constraints. |
SPC m ? |
Show all goals. |
SPC m , |
Shows the type of the goal at point and the currect context. |
SPC m . |
Shows the context, the goal and the given expression's inferred type. |
SPC m a |
Simple proof search. |
SPC m b |
Go to the previous goal, if any and activate goal-navigation micro-state. |
SPC m c |
Refine the pattern variables given in the goal. |
SPC m d |
Infers the type of the given expression. |
SPC m e |
Show the context of the goal at point. |
SPC m f |
Go to the next goal, if any and activate goal-navigation micro-state. |
SPC m h |
Compute the type of a hypothetical helper function. |
SPC m l |
Load current buffer. |
SPC m n |
Computes the normal form of the given expression, using the scope of the current goal or, if point is not in a goal, the top-level scope. |
SPC m o |
Shows all the top-level names in the given module. |
SPC m r |
Refine the goal at point. |
SPC m s |
Solves all goals that are already instantiated internally. |
SPC m t |
Show the type of the goal at point. |
SPC m x c |
Compile current module. |
SPC m x d |
Removes buffer annotations (overlays and text properties). |
SPC m x h |
Toggle display of implicit arguments. |
SPC m x q |
Quit and clean up after agda2. |
SPC m x r |
Kill and restart the agda2 buffer and load agda2-toplevel-module. |
SPC m w |
Explains why a given name is in scope. |