diff --git a/vscode-lean4/src/abbreviation/abbreviations.json b/vscode-lean4/src/abbreviation/abbreviations.json index 811e922aa..ca6cc1f64 100644 --- a/vscode-lean4/src/abbreviation/abbreviations.json +++ b/vscode-lean4/src/abbreviation/abbreviations.json @@ -1086,6 +1086,7 @@ "rbag": "⟆", "rat": "ℚ", "radioactive": "☢", + "rrbracket": "〛", "rangle": "⟩", "rq": "’", "rial": "﷼",