Zulip Chat Archive

Stream: general

Topic: Spacemacs Lean Layer

Robert Kornacki (Oct 05 2018 at 03:39):

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 (Oct 05 2018 at 03:45):

@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 (Oct 05 2018 at 03:46):

I also use Spacemacs's standard g d for navigation

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

Robert Kornacki (Oct 06 2018 at 00:30):

@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 (Oct 06 2018 at 00:31):

Great, thanks!

Last updated: Aug 03 2023 at 10:10 UTC