(set-keyboard-coding-system nil)
(global-set-key [(control h)] 'delete-backward-char)
(add-to-list 'load-path "/Users/merijn/Downloads/OPLSS/evil-evil")
(require 'evil)
(evil-mode 1)

(load-file (let ((coding-system-for-read 'utf-8))
                (shell-command-to-string "agda-mode locate")))
(custom-set-variables
 ;; custom-set-variables was added by Custom.
 ;; If you edit it by hand, you could mess it up, so be careful.
 ;; Your init file should contain only one such instance.
 ;; If there is more than one, they won't work right.
 '(agda2-include-dirs (quote ("." "/Users/merijn/Downloads/OPLSS/agda-prelude/src"))))
(custom-set-faces
 ;; custom-set-faces was added by Custom.
 ;; If you edit it by hand, you could mess it up, so be careful.
 ;; Your init file should contain only one such instance.
 ;; If there is more than one, they won't work right.
 )

(add-hook 'evil-insert-state-entry-hook
          (lambda () (set-input-method "Agda")))
(add-hook 'evil-insert-state-exit-hook
          (lambda () (set-input-method nil)))

;;; Maps C-c C-<key> to \<key in evil-normal-state
(eval-after-load 'agda2
    '(progn
        (define-prefix-command 'agda2-map)
        (global-set-key (kbd "C-g") 'agda2-map)
        (define-key agda2-map (kbd "a") 'agda2-auto)
        (define-key agda2-map (kbd "k") 'agda2-previous-goal)
        (define-key agda2-map (kbd "j") 'agda2-next-goal)
        (define-key agda2-map (kbd "c") 'agda2-make-case)
        (define-key agda2-map (kbd "d") 'agda2-infer-type-maybe-toplevel)
        (define-key agda2-map (kbd "e") 'agda2-show-context)
        (define-key agda2-map (kbd "l") 'agda2-load)
        (define-key agda2-map (kbd "n") 'agda2-compute-normalised-maybe-toplevel)
        (define-key agda2-map (kbd "o") 'agda2-module-contents-maybe-toplevel)
        (define-key agda2-map (kbd "r") 'agda2-refine)
        (define-key agda2-map (kbd "s") 'agda2-solveAll)
        (define-key agda2-map (kbd "t") 'agda2-goal-type)
        (define-key agda2-map (kbd " ") 'agda2-give)
        (define-key agda2-map (kbd ",") 'agda2-goal-and-context)
        (define-key agda2-map (kbd ".") 'agda2-goal-and-context-and-inferred)
        (define-key agda2-map (kbd "=") 'agda2-show-constraints)
        (define-key agda2-map (kbd "?") 'agda2-show-goals)
        (define-key agda2-map (kbd "xc") 'agda2-compile)
        (define-key agda2-map (kbd "xd") 'agda2-remove-annotations)
        (define-key agda2-map (kbd "xh") 'agda2-display-implicit-arguments)
        (define-key agda2-map (kbd "xl") 'agda2-load)
        (define-key agda2-map (kbd "xq") 'agda2-quit)
        (define-key agda2-map (kbd "xr") 'agda2-restart)))