Skip to content

Commit

Permalink
Removing duplicated information about Emacs mode
Browse files Browse the repository at this point in the history
  • Loading branch information
viktorcsimma authored and omelkonian committed Apr 19, 2024
1 parent 9982ec7 commit 7b3e48a
Showing 1 changed file with 3 additions and 2 deletions.
5 changes: 3 additions & 2 deletions docs/source/features.md
Original file line number Diff line number Diff line change
Expand Up @@ -1074,11 +1074,12 @@ If `implicit` is `false`, Prelude gets imported explicitly, and only those ident
# Emacs mode

Since there is a full Agda typechecker in the `agda2hs` binary,
you can readily use the Emacs mode of a pre-existing Agda installation (make sure it is the same version as the one `agda2hs` depends on) by changing the binary that `agda-mode` uses (Lisp variable `agda2-program-name`) to (the path to) `agda2hs` binary.
you can readily use the Emacs mode of a pre-existing Agda installation by changing the binary that `agda-mode` uses to the path to `agda2hs` binary.

- First, check the version of the Agda typechecker in the `agda2hs` binary by calling `agda2hs --version`.
- Install this version of Agda.
- Run `agda-mode setup` and in Emacs, set the `agda2-program-name` variable to `agda2hs` (use `M-x customize-variable`). Alternatively, you can also set it in your `~/.emacs` file by hand.
- Run `agda-mode setup`.
- In Emacs, set the `agda2-program-name` variable to `agda2hs` (use `M-x customize-variable`). Alternatively, you can also set it in your `~/.emacs` file by hand.
- With `C-c C-x C-c`, you will now be able call the `agda2hs` backend from inside Emacs; all the other built-in backends still remain available.

## Known issues
Expand Down

0 comments on commit 7b3e48a

Please sign in to comment.