vscode-lean4
vscode-lean4 copied to clipboard
leanprover
Visual Studio Code extension for the Lean 4 proof assistant
### Proposal Add hover support to defs with inherit_doc that forwards the inherited doc + type sig of current def.
### Description After clicking "mark done", the setup guide doesn't reopen when requested. ### Steps to Reproduce 1. Install the leanprover extension 2. See that it opened a helpful setup...
### Description When I right-click somewhere unrelated to "Lean InfoView", the "Lean InfoView" tab is focused. Especially, when I right-click a lean source file and choose "go to definition", the...
### Description Typically, when opening a file with a stale dependency, there is a diagnostic under 'Messages' that informs us that 'Restart File' needs to be called. However, right after...
### Proposal Oftentimes I want to work on a rather low-level file `X`. `lake exe cache get` would download me way too many files and take too long, but typing...
This PR causes indentation when hitting enter after certain tokens that appear at the end of a line. Specifically, after: * `by`, `do`, `try`, `finally`, `then`, `else`, `where`, `extends`, `deriving`,...
In VSCode, when mousing over a constant, it shows * First any errors on that constant * Below it the type of the constant Now the error is already easily...
Suppose `A.lean` has an error, and `B.lean` imports `A.lean`. If I have only `B.lean` open in VSCode, then I don't really get an actionable error. Jump to next error (F8)...
### Description When a docstring contains something that could be HTML but isn't, the rest of the file is highlighted as if it were part of the docstring. This leads...
Metadata
Owner
Metadata
Visual Studio Code extension for the Lean 4 proof assistant