This is a Spacemacs layer for the Lean theorem prover which uses Lean Mode with updated keybindings.
Lean: https://github.com/leanprover/lean Lean Mode: https://github.com/leanprover/lean-mode
| Key | Function |
|---|---|
| g d | jump to definition in source file (lean-find-definition) |
| Spc m f | jump to definition in source file (lean-find-definition) |
| Spc m , | jump back to position before M-. (xref-pop-marker-stack) |
| Spc m k | shows the keystroke needed to input the symbol under the cursor |
| Spc m xx | execute lean in stand-alone mode (lean-std-exe) |
| Spc m h | run a command on the hole at point (lean-hole) |
| Spc m d | show a searchable list of definitions (helm-lean-definitions) |
| Spc m g | toggle showing current tactic proof goal (lean-toggle-show-goal) |
| Spc m n | toggle showing next error in dedicated buffer (lean-toggle-next-error) |
| Spc m b | toggle showing output in inline boxes (lean-message-boxes-toggle) |
| Spc m r | restart the lean server (lean-server-restart) |
| Spc m s | switch to a different Lean version via elan (lean-server-switch-version) |
| Spc m a | toggle company auto-complete menu |
| Spc e n | flycheck: go to next error |
| Spc e p | flycheck: go to previous error |
| Spc e l | flycheck: show list of errors |
$ git clone https://github.com/robkorn/spacemacs-lean-layer
$ cd spacemacs-lean-layer
$ mv lean ~/.emacs.d/private/local
Then simply add 'lean' as one of your configuration layers in your spacemacs config.
After a couple hours of hunting around for why this issue exists it seems it is in relation to the lean-mode package itself. Even using lean-server-restart doesn't seem to initalize it properly. However to fix this simply toggle company auto-complete and for whatever reason Spacemacs remembers you are indeed in Vim mode and should have access to the Vim Leader Key for this major mode. This issue exists whether or not company-lean is installed.