Vim 9 plugins for Lean

Stream: Emacs

[Castedo Ellerman]

Greetings Emacslings, I come in peace from planet Vim.

Does it makes sense to have a Zulip channel for Vim/Neovim? or "NotVSCode"?

I have created documentation and a plugin for using Vim 9 to write Lean.

https://castedo.gitlab.io/vim9-lean

If anybody is writing Lean inside Vim 9 and have tips or suggestions to improve this documentation for new Vim 9 "Leaners", please feel free to share your feedback and improvements.

The Neovim plugin lean.nvim adds Lean-specific editor features whereas vim9-lean only uses Vim 9 for its generic LSP features. A separate "editor sidekick" program like Lean-TUI provides Lean specific UI features.

Although I've written documentation and a plugin specifically for Vim 9, this "editor sidekick" approach works with any editor that supports LSP. For example, @Willem vanhulle, the author of Lean-TUI, uses the editor Helix.

[Yury G. Kudryashov]

There is a thread for Neovim. You should coordinate with them first.