add abbreviations for ‖ ‖ which place the cursor inside (#315)

* add abbreviations for `∥ ∥` wich place the cursor inside * switch to better Unicode characters for norm. Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
leanprover · Nov 18, 2022 · 27898a0 · 27898a0
1 parent df7bc6e
commit 27898a0
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/src/abbreviation/abbreviations.json b/src/abbreviation/abbreviations.json
@@ -12,6 +12,8 @@
     "f<>": "‹$CURSOR›",
     "f<<>>": "«$CURSOR»",
     "[--]": "⁅$CURSOR⁆",
+    "nnnorm": "‖$CURSOR‖₊",
+    "norm": "‖$CURSOR‖",
     "\\": "\\",
     "a": "α",
     "b": "β",