From e44b9b7eb100a3d5c1640b7df7d4c458f81998ab Mon Sep 17 00:00:00 2001
From: Amin Bandali <bandali@gnu.org>
Date: Sat, 10 Nov 2018 21:20:07 -0500
Subject: [PATCH] [emacs/lean-mode] use forward slash "/" as the prefix for
 lean-input

---
 init.org | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/init.org b/init.org
index e30ed14..289b22b 100644
--- a/init.org
+++ b/init.org
@@ -1160,7 +1160,12 @@ TODO: break this giant source block down into individual org sections.
               ("S-SPC" . company-complete))
   :config
   (require 'lean-input)
-  (setq default-input-method "Lean"))
+  (setq default-input-method "Lean"
+        lean-input-tweak-all '(lean-input-compose
+                               (lean-input-prepend "/")
+                               (lean-input-nonempty))
+        lean-input-user-translations '(("/" "/")))
+  (lean-input-setup))
   #+end_src
 
 ** Haskell
-- 
2.20.1