lean.nvim
lean.nvim copied to clipboard
Julian
neovim support for the Lean theorem prover
E.g. pass this test: ```lua -- Emitted by e.g. show_term it('replaces redundant term and tactic mode', helpers.clean_buffer([[ namespace tactic.interactive meta def foo (t: itactic) : itactic := (do tactic.trace "Try...
Compare how: ``` import tactic.explode_widget #explode_widget nat.mul_comm ``` looks in VSCode: to what we render which just ends up a wall of text:
When working on mathlib in a case where olean compilation is happening in the background (e.g. with no cache, or whilst working on a lower level file), exiting neovim often...
The infoview assembles a number of subcomponents -- Tactic state, Term state, Diagnostic info, Standard error output, It may be nice to allow some customization here at some point --...
Right now a fugitive buffer from e.g. `Gdiff` on a Lean file does not connect an LSP client to the fugitive window, and therefore doesn't show infoview state.
The use case I have in mind is being able to "unfocus" the current pin so you can move around in the source, do hover requests etc. without the info...
1. Call `:LeanTermGoal` twice, this opens a floating window and moves the cursor into it. 2. Open a nested popup and move the cursor into the nested popup. (requires Lean...
The important ones are `# headlines`, `*emphasis*`, and `` `inline code` ``.
Add a configuration option `infoview.autoclose = true (default)` which indicates the infoview should be closed if no Lean buffers are updating it anymore (e.g. particularly if it is the last...
I've tried a simple nix flake setup for this plugin, but I guess I'm missing some dependencies: In https://github.com/Anderssorby/lean.nvim/tree/acs/add-nix-flake running `nix build` ``` vimplugin-lean.nvim> unpacking sources vimplugin-lean.nvim> unpacking source archive...
