vscode-lean4
vscode-lean4 copied to clipboard
leanprover
Visual Studio Code extension for the Lean 4 proof assistant
Given a file `mathlib4/aaa/bbb/ccc.lean` open in VSCode, I'd like to one-click copy the string `aaa.bbb.ccc` to the clipboard. This is useful if you want to import the current file in...
### Description (Background info: I installed [oh my zsh](https://ohmyz.sh/) on a whim and one of the things it occasionally does is prompts the user if they'd like to update when...
A reopen of #306, which was closed without explanation. I would be happy to contribute this change if it is desired.
Video demonstrating new UI / features: https://github.com/user-attachments/assets/3685f63c-c519-42f5-8f62-3978c231e60b
### Proposal Now that the hover tooltips *in the infoview* support displaying math (#534), it would be awesome if tooltips in the editor also did. Implementation-wise, it may be possible...
This PR adjusts the Windows installation script to skip the creation of a temporary file for the downloaded installer and implements better error handling for the Windows installation script. Motivated...
Added instructions for modifying abbreviation identifiers.
because `⟨n` is far more common, and instead remapped it to `\notlt` Zulip: [\
This PR adds a setup diagnostic that displays a warning if we detect that the user's OS version is unsupported for new Lean versions. The macOS version is a placeholder...
When Elan is outdated, I see the following warning message when open vscode > Lean's version manager Elan is outdated: the installed version is 3.1.1, but a version of 4.0.0...
Metadata
Owner
Metadata
Visual Studio Code extension for the Lean 4 proof assistant