feat(emacs): Basic Agda configuration

users/crumb/programs/emacs/modules/lang/syd-lang-agda.el

@@ -0,0 +1,42 @@
+;;; syd-lang-agda.el -*- lexical-binding: t; -*-
+
+(with-eval-after-load 'agda2
+  (general-define-key
+   :keymaps 'agda2-mode-map
+   :states '(normal visual motion emacs insert)
+   :major-modes t
+   :prefix syd-localleader-key
+   :non-normal-prefix syd-alt-localleader-key
+   "?" #'agda2-show-goals
+   "." #'agda2-goal-and-context-and-inferred
+   "," #'agda2-goal-and-context
+   "=" #'agda2-show-constraints
+   "SPC" #'agda2-give
+   "a" #'agda2-mimer-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
+   "x c" #'agda2-compile
+   "x d" #'agda2-remove-annotations
+   "x h" #'agda2-display-implicit-arguments
+   "x q" #'agda2-quit
+   "x r" #'agda2-restart)
+  (general-def
+    :keymaps 'agda2-mode-map
+    :states '(motion normal)
+    "[ n" #'agda2-previous-goal
+    "] n" #'agda2-next-goal)
+  (setq agda2-fontset-name "JuliaMono"))
+
+(provide 'syd-lang-agda)