c3866382b2
- Add #+HTML_HEAD_EXTRA options to all org files - HTMLize published documentation via CSS
5.3 KiB
5.3 KiB
Agda contribution layer for Spacemacs
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. For
information about setting up $PATH, check out the corresponding section in the
FAQ (SPC f e h $PATH RET).
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 p |
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. |