The input method (“Lean”) for major mode
lean4-mode triggers autocompletion for various unicode symbols, and doesn’t activate by default when I open a Lean4 buffer/project; I have to do
M-x toggle-input-method to activate it for every Lean4 buffer where I want the input method.
Per this stackoverflow answer, I’d like to fix that by triggering
(activate-input-method "Lean") in any buffer where
lean4-mode is the major mode. In my
config.el, I have
(after! lean4-mode (add-hook 'lean4-mode-hook (lambda () (activate-input-method "Lean"))))
This does not appear to cause any change to the input method or trigger any errors or logs that I can see in
I expect the input method to change when I switch to any buffer with the
lean4-mode major mode.
lean4-mode, per repo instructions appropriate for your emacs/doom-emacs/system config.
- Add the hook above to
- Create a Lean4 project.
- Open a Lean4 file in that project and either look for the
Leaninput method symbol in the modeline (
Π) or attempt to trigger autocompletion.
If autocomplete is working, then there should be a
Π in the modeline and e.g.
\alpha should autocomplete to
α. If the
Lean input method is not active, there will be no
Π in the modeline and
\alpha will simply remain as-is in the buffer.
Loading data dump...