spacemacs/contrib/!lang/agda

Agda contribution layer for Spacemacs

• Table of Contents
• Description
  • Some features:
• Install
  • Layer
  • Agda
• Key bindings

Table of Contents   TOC@4

• Description

  • Some features:

• Install

  • Layer
  • Agda
• Key bindings

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.