Skip to content

Commit bd30f68

Browse files
authored
feat: alias \dot and \cdot to \centerdot (#639)
Discussed at [#lean4 > \cdot != \centerdot @ 💬](https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/.5Ccdot.20!.3D.20.5Ccenterdot/near/528312220).
1 parent 1590e3b commit bd30f68

File tree

1 file changed

+2
-2
lines changed

1 file changed

+2
-2
lines changed

lean4-unicode-input/src/abbreviations.json

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -492,7 +492,7 @@
492492
"doteq": "",
493493
"dotplus": "",
494494
"dotsquare": "",
495-
"dot": "",
495+
"dot": "·",
496496
"dong": "",
497497
"downarrow": "",
498498
"downdownarrows": "",
@@ -991,7 +991,7 @@
991991
"colon": "",
992992
"copyright": "©",
993993
"cdots": "",
994-
"cdot": "",
994+
"cdot": "·",
995995
"cib": "",
996996
"ciw": "",
997997
"ci..": "",

0 commit comments

Comments
 (0)