agda2-mode

A major mode for editing Agda (the dependently typed programming
language / interactive theorem prover).

Major features include:

- syntax highlighting.

- on the fly Agda interpretation.

- goal-driven development

- interactive case-splitting

- proof search

- input support (for utf8 characters)

see https://agda.readthedocs.io/ for more information


Dependency