Skip to content

Neovim

Note

There is little reason to use Webleank or Lspleank with Neovim. The Julian/lean.nvim plugin is more stable and full-featured.

You can try Lspleank with Neovim by adding the following lines to your ~/.config/nvim/init.lua file (or similar config file):

vim.lsp.config['lean_ls'] = {
  cmd = { 'lspleank', 'lake' },
  filetypes = { 'lean' },
}

vim.lsp.enable('lean_ls')

For more information visit https://neovim.io/doc/user/lsp/.