Having both `\centerdot` (aka `\.`) and `\cdot` can be unnecessarily confusing.

The context is I was trying to quickly confirm that match · works, but ended up typing match ⬝ instead:

The reason I ended up with the second form (the square one, i.e. U+2B1D) is that I was typing \cdot, which is what I'm used to from other LaTeX IMEs (where I've only seen it result in the same thing as Lean4's \centerdot, i.e. U+00B7).

It was very confusing at first, until I tried simpler usecases of the · lambda shorthands and nothing worked.

After copying the correct character from the Lean4 manual, I saw that it said this on hover:

Type · using \. or \centerdot

Whereas the "wrong" (square) one had this instead:

Type ⬝ using \tr or \dot or \con or \cdot

Sadly there's nothing even in that description to indicate it's the wrong thing (i.e. it seems to claim it's a "dot" even when it's not, it's a square, "Black Very Small Square" according to Unicode), and visual inspection requires a font size large enough to make the squareness obvious (which I don't usually have in VSCode).

Maybe it's not that useful on average, but perhaps having the Unicode name in the hover text could be an improvement? (Lean4 itself detecting confusables would be neat but probably way more involved).

The "obvious" suggestion here is changing some of these abbreviations, but I'm not sure how much breaking changes are considered, and/or what the usage of some of these these abbreviations even looks like in practice.

cc @Kha (because I came across you calling \. aka \centerdot, "cdot" while looking for existing issues)

Start by locating the VS Code extension code that provides hover text and resolves Unicode input abbreviations for \centerdot, \cdot, and related forms. Review the existing behavior described in issue #308 and determine which specific change is intended before implementing it. Done should include a decided treatment of the confusing abbreviations and hover text, with regression coverage if the project has relevant tests.