Unnamed repository; edit this file 'description' to name the repository.
remove ' and add ⟨⟩ in lean autopairs (#10688)
| -rw-r--r-- | languages.toml | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/languages.toml b/languages.toml index ecf1b49f..ec3e36ed 100644 --- a/languages.toml +++ b/languages.toml @@ -1040,6 +1040,13 @@ block-comment-tokens = { start = "/-", end = "-/" } language-servers = [ "lean" ] indent = { tab-width = 2, unit = " " } +[language.auto-pairs] +'(' = ')' +'{' = '}' +'[' = ']' +'"' = '"' +'⟨' = '⟩' + [[grammar]] name = "lean" source = { git = "https://github.com/Julian/tree-sitter-lean", rev = "d98426109258b266e1e92358c5f11716d2e8f638" } |