From 63caac0fd014bcea5258fe617a00ae0db06478b1 Mon Sep 17 00:00:00 2001 From: Julian Berman Date: Tue, 10 Sep 2024 03:39:35 -0400 Subject: [PATCH] feat: add double parens abbreviations (#523) Corresponds to [[ and {{ -- they aren't used (yet) in Mathlib but would potentially be used for LaurentSeries notation. --- lean4-unicode-input/src/abbreviations.json | 3 +++ 1 file changed, 3 insertions(+) diff --git a/lean4-unicode-input/src/abbreviations.json b/lean4-unicode-input/src/abbreviations.json index 326b54d86..712162bc9 100644 --- a/lean4-unicode-input/src/abbreviations.json +++ b/lean4-unicode-input/src/abbreviations.json @@ -9,6 +9,7 @@ "()": "($CURSOR)", "()_": "($CURSOR)_", "([])'": "⟮$CURSOR⟯", + "(())": "⸨$CURSOR⸩", "f<>": "‹$CURSOR›", "f<<>>": "«$CURSOR»", "[--]": "⁅$CURSOR⁆", @@ -1179,6 +1180,8 @@ "]]": "⟧", "{{": "⦃", "}}": "⦄", + "((": "⸨", + "))": "⸩", "([": "⟮", "])": "⟯", "Xi": "Ξ",