lean.nvim
lean.nvim copied to clipboard
Julian
neovim support for the Lean theorem prover
Hi! I'd like to only load the `lean.nvim` plugin if im editing a lean file. I'm currently using the packer package manager, so I did ```lua use { 'Julian/lean.nvim', ft...
Lean 4 shows inaccessible hypotheses with a trailing cross symbol. Emacs and VSCode treat these by doing one or both of eliding the cross symbol and highlighting the hypotheses in...
It's quite annoying to search for non-ASCII characters via `/`, for instance, because you have to have yanked the character you're looking for ahead of time. Possibly there's some solution...
Depends on (minor) bug fixes in phaazon/hop.nvim#304. What I've done so far is to map: - `jj` to hop to interactive elements of the infoview - `jd` to use the...
Users occasionally will put this in a file they reload or re-source, so it'd be nice if it were able to be run multiple times. Right now most of the...
Hey, I've just started using Lean 4 and often get the error: `Client 1 quit with exit code 1 and signal 0` when I start editing. Not sure if it's...
Right now if the infoview contents are too long, we show the top lines. It seems more natural perhaps to show the goal instead, which is almost the bottom modulo...
~~I am assuming this is ARM-specific, otherwise I presume otherwise it'd be reported by others, but I often get segmentation faults in buffers with Lean 3.~~ This now seems not-OS...
Putting this here off the back of / in order to track [this Zulip request](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/lean.2Envim/near/280738234). I want to be able to configure Infoview updates to be less "jittery" (and possibly...
See https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Parser.20Expression.20Grammars.20.28PVS.20and.20Lean.20comparison.29/near/279170568 Perhaps a simple thing we could do is just show a horizontal rule (i.e. a line) below any instance of this tactic.