Spacemacs Lean Layer

Stream: general

[Robert Kornacki]

Recently I just quickly put together a Spacemacs layer for lean which pretty much just rebinds lean-mode to be as expected for the Spacemacs vim crowd. Thought it'd be worth sharing for anyone else who's a Spacemacs user https://github.com/robkorn/spacemacs-lean-layer

[Sebastian Ullrich]

@Robert Kornacki Looks nice! Here's some more config from my .spacemacs file:

  (push 'lean-mode spacemacs-indent-sensitive-modes)

  (sp-local-pair 'lean-mode "/-" "-/")
  (sp-local-pair 'lean-mode "`'" nil :actions :rem)
  (sp-local-pair 'lean-mode "⟨" "⟩")
  (sp-local-pair 'lean-mode "«" "»")
  ;; etc, haven't bothered to complete the list yet

[Sebastian Ullrich]

I also use Spacemacs's standard g d for navigation

  (spacemacs|define-jump-handlers lean-mode (lean-find-definition :async t))

[Robert Kornacki]

@Sebastian Ullrich Ah, thanks for sharing! I've added all of your config to the layer since they are no-brainers to include. As I keep using lean and find the need to I'll most likely keep adding local-pairs overtime. If you or anyone else comes up with something else to add let me know or shoot me a pull request.

[Sebastian Ullrich]

Great, thanks!