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 pressingEnter
next to a quote ("
)wordPattern
- removes the dot (.), so that fully qualified Lean names become "words"- Example:
Mathlib.Data.List.Sort
becomes a "word"
- Example:
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.