I remember the last time I was trying to get into proof assistants, I was discouraged by the lack of functionality for vim users. At the time, it seemed like a lot of powerful features (holes, etc) worked best with Emacs, and had only limited support (if any support at all) in vim. Unfortunately, this was so discouraging that I never actually learned how to use any theorem provers (I'm aware of evil, but it also seemed like a hassle).
But now a few years have passed, and with the growing popularity of Neovim (which adds a lot of modern functionality), it seems reasonable that the state of things might have changed (or at least, that it might be changing). As some evidence for this, I saw a recent blog post about cornelis, which promises to bring many of the Agda features from Emacs to Neovim.
I'm excited about theorem provers again, and seeing this blog post has given me hope that there might be other resources for vim users that I wasn't able to find with a cursory google (even googling "cornelius agda" doesn't bring up the above project on the first page). Which brings me to the main question I have:
If you are a (Neo)vim user, which theorem prover(s) do you use? Moreover, how do you interact with it? Does the experience feel fully featured?
If there are any nice guides on getting things up and running for a Vim user, I would also be interested in those. The nice thing about being new to all this is that I'm currently language-agnostic, and I would be happy to learn any of the major languages.
Thanks in advance! ^_^