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

[eddyb]

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)

[eternaleye]

Somewhat frustratingly, the LaTeX unicode-math package disagrees with both interpretations, giving U+00B7 MIDDLE DOT the name \cdotp, while U+22C5 DOT OPERATOR gets to claim \cdot.

From the manual:

[Kha]

The reason it is called "cdot" internally is because that is the/an Emacs mapping, or at least it was until we adopted the VS Code extension's abbreviation table. I didn't really notice because I always use \.. It might help to ask on Zulip what people use to enter the square, but I agree that anything containing "dot" for it is confusing and having different mappings for cdot and centerdot is even more so.