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.