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/README.org
justbur 6eab954afe Use + instead of ! for layer categories 
Helm seems to treat "!" specially in pattern matching, so having a ! in
the pattern string when traversing directories is problematic. This
change fixes #2737, because as far as I can tell "+" has no special
meaning in a helm pattern.

Of course, we can choose a different character, but I'm fond of "+" as
representing "more layers here".
2015-09-11 00:13:51 -04:00

5.1 KiB
Raw Blame History

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 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.