From dbf9e9e2c7cf3a3c56ad398cfe3ce43407bbacd4 Mon Sep 17 00:00:00 2001
From: Rudi Grinberg <rudi.grinberg@gmail.com>
Date: Sat, 7 Sep 2019 02:18:51 +0900
Subject: [PATCH] Add a module for the lean theorem prover

Signed-off-by: Rudi Grinberg <rudi.grinberg@gmail.com>
---
 modules/lang/lean/config.el   | 33 +++++++++++++++++++++++++++++++++
 modules/lang/lean/packages.el |  7 +++++++
 2 files changed, 40 insertions(+)
 create mode 100644 modules/lang/lean/config.el
 create mode 100644 modules/lang/lean/packages.el

diff --git a/modules/lang/lean/config.el b/modules/lang/lean/config.el
new file mode 100644
index 000000000..faf37150c
--- /dev/null
+++ b/modules/lang/lean/config.el
@@ -0,0 +1,33 @@
+;;; lang/lean/config.el -*- lexical-binding: t; -*-
+
+(use-package! company-lean
+  :when (featurep :completion 'company)
+  :after lean-mode
+  :config (set-company-backend! 'lean-mode 'company-lean))
+
+(use-package! lean-mode
+  :config
+  (set-lookup-handlers! 'lean-mode
+    :definition #'lean-find-definition)
+  (sp-with-modes 'lean-mode
+    (sp-local-pair "/-" "-/")
+    (sp-local-pair "`'" nil :actions :rem)
+    (sp-local-pair "{" "}")
+    (sp-local-pair "«" "»"))
+  (map!
+   :map lean-mode-map
+   :localleader
+   "g" #'lean-toggle-show-goal
+   "n" #'lean-toggle-next-error
+   (:prefix "s"
+     "r" #'lean-server-restart
+     "s" #'lean-server-stop
+     "v" #'lean-server-switch-version)
+   (:prefix "p"
+     "t" #'lean-leanpkg-test
+     "b" #'lean-leanpkg-build
+     "c" #'lean-leanpkg-configure)
+   "f" #'lean-fill-placeholder
+   "h" #'lean-hole
+   "m" #'lean-message-boxes-toggle
+   "e" #'lean-execute))
diff --git a/modules/lang/lean/packages.el b/modules/lang/lean/packages.el
new file mode 100644
index 000000000..6061c61f6
--- /dev/null
+++ b/modules/lang/lean/packages.el
@@ -0,0 +1,7 @@
+;; -*- no-byte-compile: t; -*-
+;;; lang/lean/packages.el
+
+(package! lean-mode)
+
+(when (featurep! :completion company)
+  (package! company-lean))