TakeV/spacemacs
Archived
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity
This repository has been archived on 2024-10-22. You can view files and clone it, but cannot push or open issues or pull requests.
spacemacs/layers/+lang/agda
History
Eivind Fonn c893383fe4 Fix some documentation bugs 
- CSS links
- GIFS in published version
- Unify layer doc titles
- Change emoji layer emojis to an image
2015-12-03 23:50:29 -05:00
..
extensions.el layers: Transition to new key bindings functions 2015-11-21 18:22:51 +01:00
README.org Fix some documentation bugs 2015-12-03 23:50:29 -05:00

README.org

Agda layer

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.