From 2e7aa30f7e46eabf984adc1018d7ccbdfefecca8 Mon Sep 17 00:00:00 2001
From: Amin Bandali <bandali@gnu.org>
Date: Mon, 29 Oct 2018 23:28:22 -0400
Subject: [PATCH] [emacs] use lean-input as default input method, toggled with
 C-\
MIME-Version: 1.0
Content-Type: text/plain; charset=utf8
Content-Transfer-Encoding: 8bit

super handy for inserting logical symbols like ∧,∨,→,↔,≡,≜,∩,∪,λ,∘,⋯
---
 init.org | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/init.org b/init.org
index 75e92ee..3448670 100644
--- a/init.org
+++ b/init.org
@@ -1134,9 +1134,13 @@ TODO: break this giant source block down into individual org sections.
 #+begin_src emacs-lisp
 (eval-when-compile (defvar lean-mode-map))
 (use-package lean-mode
+  :defer 2
   :bind (:map lean-mode-map
-              ("S-SPC" . company-complete)))
-#+end_src
+              ("S-SPC" . company-complete))
+  :config
+  (require 'lean-input)
+  (setq default-input-method "Lean"))
+  #+end_src
 
 ** Haskell
 
-- 
2.20.1