From 818df0afe437cb64c6cd0d550f20805cec63ac96 Mon Sep 17 00:00:00 2001
From: Patrick Elliott <patrick.d.elliott@gmail.com>
Date: Mon, 3 Sep 2018 16:11:08 +0200
Subject: [PATCH] More keybindings

---
 modules/lang/agda/config.el | 30 ++++++++++++++++++++++++------
 1 file changed, 24 insertions(+), 6 deletions(-)

diff --git a/modules/lang/agda/config.el b/modules/lang/agda/config.el
index 5ae19aca1..dce22f3a0 100644
--- a/modules/lang/agda/config.el
+++ b/modules/lang/agda/config.el
@@ -41,9 +41,27 @@
            (agda2-highlight-typechecks-face              . font-lock-warning-face))))
   :config
   (map! :map agda2-mode-map
-                :localleader
-                :n "l" #'agda2-load
-                :n "d" #'agda2-infer-type-maybe-toplevel
-                :n "o" #'agda2-module-contents-maybe-toplevel
-                :n "n" #'agda2-compute-normalised-maybe-toplevel))
-  ;; TODO finish keybindings
+        :localleader
+        :n "?"  #'agda2-show-goals
+        :n "."  #'agda2-goal-and-context-and-inferred
+        :n ","   #'agda2-goal-and-context
+        :n "="   #'agda2-show-constraints
+        :n "SPC" #'agda2-give
+        :n "a"   #'agda2-auto
+        :n "c"   #'agda2-make-case
+        :n "d"   #'agda2-infer-type-maybe-toplevel
+        :n "e"   #'agda2-show-context
+        :n "gG"  #'agda2-go-back
+        :n "h"   #'agda2-helper-function-type
+        :n "l"   #'agda2-load
+        :n "n"  #'agda2-compute-normalised-maybe-toplevel
+        :n "p"  #'agda2-module-contents-maybe-toplevel
+        :n "r"  #'agda2-refine
+        :n "s"  #'agda2-solveAll
+        :n "t"  #'agda2-goal-type
+        :n "w"  #'agda2-why-in-scope-maybe-toplevel
+        :n "xc" #'agda2-compile
+        :n "xd" #'agda2-remove-annotations
+        :n "xh" #'agda2-display-implicit-arguments
+        :n "xq" #'agda2-quit
+        :n "xr" #'agda2-restart))