Slacker News Slacker News logo featuring a lazy sloth with a folded newspaper hat
  • top
  • new
  • show
  • ask
  • jobs
Library
← Back to context

Comment by heliumtera

3 hours ago

>The recommended way to install Lean is through VS Code and the Lean 4 VS Code extension,

Lol

2 comments

heliumtera

Reply

jinwoo68  1 hour ago

There are community-built editor supports. For example,

- Emacs: https://github.com/leanprover-community/lean4-mode

- Neovim: https://github.com/Julian/lean.nvim

I'm using the Emacs lean4-mode and it's pretty good.

adamnemecek  1 hour ago

It makes complete sense to polish that usecase.

Slacker News

Product

  • API Reference
  • Hacker News RSS
  • Source on GitHub

Community

  • Support Ukraine
  • Equal Justice Initiative
  • GiveWell Charities