c3866382b2
- Add #+HTML_HEAD_EXTRA options to all org files - HTMLize published documentation via CSS
72 lines
5.3 KiB
Org Mode
72 lines
5.3 KiB
Org Mode
#+TITLE: Agda contribution layer for Spacemacs
|
|
#+HTML_HEAD_EXTRA: <link rel="stylesheet" type="text/css" href="../../../css/readtheorg.css" />
|
|
|
|
* Table of Contents :TOC_4_org:noexport:
|
|
- [[Description][Description]]
|
|
- [[Some features:][Some features:]]
|
|
- [[Install][Install]]
|
|
- [[Layer][Layer]]
|
|
- [[Agda][Agda]]
|
|
- [[Key bindings][Key bindings]]
|
|
|
|
* Description
|
|
This layer adds support for the [[http://wiki.portal.chalmers.se/agda/pmwiki.php][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=
|
|
|
|
#+BEGIN_SRC emacs-lisp
|
|
(setq-default dotspacemacs-configuration-layers '(agda))
|
|
#+END_SRC
|
|
|
|
** Agda
|
|
Quick instructions to install Agda assuming you have cabal installed:
|
|
|
|
#+BEGIN_SRC sh
|
|
cabal install alex happy "cpphs < 1.19" agda
|
|
#+END_SRC
|
|
|
|
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. |
|