88fc054919
We can fetch the mode directly from straight. There's no need to rely on having this .el file installed for us. Now agda's el files can be edited directly like all other emacs packages. Signed-off-by: Rudi Grinberg <rudi.grinberg@gmail.com>
32 lines
902 B
EmacsLisp
32 lines
902 B
EmacsLisp
;;; lang/agda/config.el -*- lexical-binding: t; -*-
|
|
|
|
(map!
|
|
:after agda2-mode
|
|
:map agda2-mode-map
|
|
:localleader
|
|
"?" #'agda2-show-goals
|
|
"." #'agda2-goal-and-context-and-inferred
|
|
"," #'agda2-goal-and-context
|
|
"=" #'agda2-show-constraints
|
|
"SPC" #'agda2-give
|
|
"a" #'agda2-auto-maybe-all
|
|
"b" #'agda2-previous-goal
|
|
"c" #'agda2-make-case
|
|
"d" #'agda2-infer-type-maybe-toplevel
|
|
"e" #'agda2-show-context
|
|
"f" #'agda2-next-goal
|
|
"gG" #'agda2-go-back
|
|
"h" #'agda2-helper-function-type
|
|
"l" #'agda2-load
|
|
"n" #'agda2-compute-normalised-maybe-toplevel
|
|
"p" #'agda2-module-contents-maybe-toplevel
|
|
"r" #'agda2-refine
|
|
"s" #'agda2-solveAll
|
|
"t" #'agda2-goal-type
|
|
"w" #'agda2-why-in-scope-maybe-toplevel
|
|
(:prefix "x"
|
|
"c" #'agda2-compile
|
|
"d" #'agda2-remove-annotations
|
|
"h" #'agda2-display-implicit-arguments
|
|
"q" #'agda2-quit
|
|
"r" #'agda2-restart))
|