#+TITLE: Agda layer
#+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 configuration layer, add it to your =~/.spacemacs=. You will need to
add =agda= to the existing =dotspacemacs-configuration-layers= list in this
file.

** 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 h SPC $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 transient-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 transient-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.                                                                                                    |