Shorter abbreviation for ·

Stream: lean4

[Gabriel Ebner]

I'd like suggestions for a shorter abbreviation for ·, like in (· + ·). Unfortunately, \cdot is already taken for ⬝ (which is a different unicode symbol). I'm getting tired of typing \centerdot.

[Mario Carneiro]

I discovered that . also works

[Mario Carneiro]

I use that now

[Mario Carneiro]

(that's a plain period character fyi)

[Sebastian Ullrich]

In Emacs it's

             to input: type "\centerdot" or "\cdot" or "\dot" or "\." with Lean input method

[Gabriel Ebner]

If nobody objects, then we can also make ⬝ and ∙ expand into · (yes, these are three different unicode dots!).

[Mario Carneiro]

I would prefer for lean not to take any of the center dots and just use . for this syntax. Let the mathematicians have the dots

[Gabriel Ebner]

There's a pretty common case where the ASCII dot doesn't work, namely in dot-notation: [(1,2)].map (·.fst)

[Gabriel Ebner]

Should we just make ∙ expand into · instead?

[Gabriel Ebner]

That's \.

[Mario Carneiro]

Can we make either (..fst) or (. .fst) work?