From 2e7aa30f7e46eabf984adc1018d7ccbdfefecca8 Mon Sep 17 00:00:00 2001 From: Amin Bandali Date: Mon, 29 Oct 2018 23:28:22 -0400 Subject: [PATCH 1/1] [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