upvote
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.

reply
It makes complete sense to polish that usecase.
reply