Use map! with after! to setup bindings

Signed-off-by: Rudi Grinberg <rudi.grinberg@gmail.com>

modules/lang/lean/config.el

@@ -1,29 +1,24 @@
 ;;; lang/lean/config.el -*- lexical-binding: t; -*-
 
-(use-package! company-lean
+(after! lean-mode
-  :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 "{" "}")
-    (sp-local-pair "«" "»"))
+    (sp-local-pair "«" "»")
-  (map!
+    (sp-local-pair "⟨" "⟩")
-   :map lean-mode-map
+    (sp-local-pair "⟪" "⟫"))
+  (map! :map lean-mode-map
         :localleader
         "g" #'lean-toggle-show-goal
         "n" #'lean-toggle-next-error
-   (:prefix "s"
+        (:prefix ("s" . "server")
           "r" #'lean-server-restart
           "s" #'lean-server-stop
           "v" #'lean-server-switch-version)
-   (:prefix "p"
+        (:prefix ("p" . "leanpkg")
           "t" #'lean-leanpkg-test
           "b" #'lean-leanpkg-build
           "c" #'lean-leanpkg-configure)
@@ -31,3 +26,9 @@
         "h" #'lean-hole
         "m" #'lean-message-boxes-toggle
         "e" #'lean-execute))
+
+
+(use-package! company-lean
+  :when (featurep! :completion company)
+  :after lean-mode
+  :config (set-company-backend! 'lean-mode 'company-lean))