Skip to content
| Marketplace
Sign in
Visual Studio Code>Snippets>Lean 4 Custom Language ConfigurationNew to Visual Studio Code? Get it now.
Lean 4 Custom Language Configuration

Lean 4 Custom Language Configuration

Denis Gorbachev

|
442 installs
| (0) | Free
Add backticks to closing & surrounding pairs
Installation
Launch VS Code Quick Open (Ctrl+P), paste the following command, and press enter.
Copied to clipboard
More Info

VSCode Lean 4 Custom Language Configuration

Features

This extension overrides the following language configuration properties:

  • autoClosingPairs - adds backticks (`)
  • surroundingPairs - adds backticks (`)
  • onEnterRules - adds a rule to skip indenting the new line after pressing Enter next to a quote (")
  • wordPattern - removes the dot (.), so that fully qualified Lean names become "words"
    • Example: Mathlib.Data.List.Sort becomes a "word"

Gotchas:

  • This extension applies some parts of its language configuration after a 250ms timeout. This is a hack to ensure that it overrides the main extension (lean4). This hack is required because there's no way to specify the extension load order to ensure that this extension always overrides the main extension.
  • Contact us
  • Jobs
  • Privacy
  • Manage cookies
  • Terms of use
  • Trademarks
© 2025 Microsoft