Skip to content

Commit 912ca19

Browse files
authored
feat: add a second two sided abbreviation for ‖z‖ (#634)
We already have `norm`, but this matches the convention for other "bracketed" abbreviations where `\<opening><closing>` produces `<opening>$CURSOR<closing>`.
1 parent dadb4e4 commit 912ca19

File tree

1 file changed

+1
-0
lines changed

1 file changed

+1
-0
lines changed

lean4-unicode-input/src/abbreviations.json

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,7 @@
1313
"f<>": "‹$CURSOR›",
1414
"f<<>>": "«$CURSOR»",
1515
"[--]": "⁅$CURSOR⁆",
16+
"||||": "‖$CURSOR‖",
1617
"nnnorm": "‖$CURSOR‖₊",
1718
"norm": "‖$CURSOR‖",
1819
"floor": "⌊$CURSOR⌋",

0 commit comments

Comments
 (0)