lean.nvim
lean.nvim copied to clipboard
Julian
neovim support for the Lean theorem prover
In simple cases I think there are simple changes we can make. E.g. probably we should `set indentkeys+==where` and `:=` for Lean 4. For more complex cases, if or when...
Given a sequence of tactics, load the goal state text at the end of each tactic into the quickfix list and allow a sequential (text) vimdiff of the state from...
Maybe it'd be nice (and reasonably easy?) to have a list of simp-normal forms and to highlight non-simp-normal terms as warnings. Zulip and the docs have an existing list of...
Given multiple different suggestions in the diagnostics, it's probably better to decide which to insert via a normal pum / completion selection.
The main motivation for this is that it makes the goal visible when the infoview is full of many lines (e.g. there are many hypotheses). In particular this happens a...
Put the following in a lakefile: ```lean require std4 from git "https://github.com/leanprover-community/std4" @ "main" ``` Note that I made a mistake: this repo does not exist since `std4` is in...
https://github.com/neovim/neovim/issues/12517
The built-in LSP hover handler properly renders hover popups as markdown, e.g.:  But our custom popups in the infoview (for tooltips) do not,...
Particularly ones from https://github.com/leanprover/vscode-lean4/pull/302/files