Evil + lean-mode

Stream: general

[Adam Topaz]

I'm trying to set up emacs to work with lean. I use evil for vim bindings, along with evil-leader (set as SPC). Has anyone been able to get company-lean to work with evil-leader? Here is what I have in my config:

(evil-leader/set-key-for-mode 'lean-mode
  "s" 'company-complete
  )

This doesn't seem to work. Does anyone have any suggestions?

[Patrick Massot]

I think vim users that want to use emacs for Lean rather use spacemacs.

[Patrick Massot]

Hopefully search Zulip for spacemacs will give results.

[Adam Topaz]

Spacemacs is too bloated for my taste :(

[Adam Topaz]

I guess I can look at the code for the lean spacemacs layer.

[Adam Topaz]

Hmmm... https://github.com/robkorn/spacemacs-lean-layer/blob/master/lean/packages.el suggests that evil-leader should just work.

[Adam Topaz]

Ah, the code above does just work. It was some other issue with my configuration of evil-leader. Forget everything I said.

[Adam Topaz]

escape > control