Hi Julian, thanks for your work on this plugin! I've been enjoying it quite a lot for my work with lean4 over the past several weeks.
I'd like to suggest this change because initially I failed to notice the slightly different plugin list over at https://github.com/Julian/lean.nvim/wiki/Getting-Started, so I didn't get completion working until today. If you don't install these additional plugins, completion fails silently. I managed to waste some time thinking something was wrong with my lua config before ultimately reading the documentation for nvim-cmp.
Hi Julian, thanks for your work on this plugin! I've been enjoying it quite a lot for my work with lean4 over the past several weeks.
I'd like to suggest this change because initially I failed to notice the slightly different plugin list over at https://github.com/Julian/lean.nvim/wiki/Getting-Started, so I didn't get completion working until today. If you don't install these additional plugins, completion fails silently. I managed to waste some time thinking something was wrong with my lua config before ultimately reading the documentation for
nvim-cmp
.