2018-08-21 12:46:29 +02:00
|
|
|
;;; lang/agda/config.el -*- lexical-binding: t; -*-
|
|
|
|
|
|
2018-08-22 03:52:53 +02:00
|
|
|
(defvar +agda-dir
|
2018-08-22 03:53:19 +02:00
|
|
|
(when (executable-find "agda-mode")
|
2018-08-25 17:27:42 +02:00
|
|
|
(file-name-directory (shell-command-to-string "agda-mode locate"))))
|
2018-08-21 12:46:29 +02:00
|
|
|
|
2018-09-21 14:52:42 +02:00
|
|
|
(def-package! agda2
|
|
|
|
|
:when +agda-dir
|
2018-08-25 17:27:42 +02:00
|
|
|
:load-path +agda-dir)
|
2018-08-21 12:46:29 +02:00
|
|
|
|
2018-08-25 17:27:42 +02:00
|
|
|
(def-package! agda2-mode
|
2018-09-21 14:52:42 +02:00
|
|
|
:defer t
|
2018-08-25 17:27:42 +02:00
|
|
|
:config
|
|
|
|
|
(map! :map agda2-mode-map
|
2018-09-03 16:11:08 +02:00
|
|
|
:localleader
|
2018-12-23 23:54:27 -05:00
|
|
|
"?" #'agda2-show-goals
|
|
|
|
|
"." #'agda2-goal-and-context-and-inferred
|
|
|
|
|
"," #'agda2-goal-and-context
|
|
|
|
|
"=" #'agda2-show-constraints
|
|
|
|
|
"SPC" #'agda2-give
|
|
|
|
|
"a" #'agda2-auto
|
|
|
|
|
"c" #'agda2-make-case
|
|
|
|
|
"d" #'agda2-infer-type-maybe-toplevel
|
|
|
|
|
"e" #'agda2-show-context
|
|
|
|
|
"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)))
|
