-
Notifications
You must be signed in to change notification settings - Fork 1
/
extensions.el
60 lines (56 loc) · 1.86 KB
/
extensions.el
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
;;; extensions.el --- agda Layer extensions File for Spacemacs
;;
;; Copyright (c) 2012-2014 Sylvain Benner
;; Copyright (c) 2014-2015 Sylvain Benner & Contributors
;;
;; Author: Sylvain Benner <sylvain.benner@gmail.com>
;; URL: https://github.com/syl20bnr/spacemacs
;;
;; This file is not part of GNU Emacs.
;;
;;; License: GPLv3
(defvar agda-pre-extensions
'(
;; pre extension agdas go here
)
"List of all extensions to load before the packages.")
(defvar agda-post-extensions '(
)
"List of all extensions to load after the packages.")
(load-file (let ((coding-system-for-read 'utf-8))
(shell-command-to-string "agda-mode locate")))
(evil-leader/set-key-for-mode 'agda2-mode
"mm" 'agda2-load
"mC" 'agda2-compile
"mQ" 'agda2-quit
"mR" 'agda2-restart
"mD" 'agda2-remove-annotations
"mim" 'agda2-display-implicit-arguments
"m=" 'agda2-show-constraints
"ms" 'agda2-solve-constraints
"m?" 'agda2-show-goals
"mj" 'agda2-next-goal
"mk" 'agda2-previous-goal
"mg" 'agda2-give
"mr" 'agda2-refine
"ma" 'agda2-auto
"mc" 'agda2-make-case
"mt" 'agda2-goal-type
"me" 'agda2-show-context
"mh" 'agda2-helper-function-type
"md" 'agda2-infer-type-maybe-toplevel
"mw" 'agda2-why-in-scope-maybe-toplevel
"m," 'agda2-goal-and-context
"m." 'agda2-goal-and-context-and-inferred
"mo" 'agda2-module-and-contents-maybe-toplevel
"mn" 'agda2-compute-normalised-maybe-toplevel
)
;; For each extension, define a function agda/init-<extension-agda>
;;
;; (defun agda/init-my-extension ()
;; "Initialize my extension"
;; )
;;
;; Often the body of an initialize function uses `use-package'
;; For more info on `use-package', see readme:
;; https://github.com/jwiegley/use-package