add definition lookup handler to agda module
This commit is contained in:
parent
1456108d5b
commit
1fa4516cad
1 changed files with 31 additions and 30 deletions
|
@ -7,33 +7,34 @@
|
|||
(unless (require 'agda2 nil t)
|
||||
(message "Failed to find the `agda2' package")))
|
||||
|
||||
|
||||
(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))
|
||||
(after! agda2-mode
|
||||
(set-lookup-handlers! 'agda2-mode
|
||||
:definition #'agda2-goto-definition-keyboard)
|
||||
(map! :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)))
|
||||
|
|
Loading…
Add table
Add a link
Reference in a new issue