Unicode abbreviations in vim/nvim

Stream: new members

[mars0i]

Sorry to ask--I know this is a faq, but it's difficult to search on, both in the Lean world and in the wider web.

Is there a cheatsheet or reference for easy ways to enter Unicode that's widely used in Lean? For example, I learned from this page how to create prefix "sections" from operators, but then I have to figure out how to enter the character · . After some investigation, I happened to see that I can enter in vim/nvim with C-v ub7, but surely there's an easier and more memorable way. (My first attempt was the LaTeX command \cdot, but that's not the correct character--something for another post.)

[Henrik Böving]

I assume you are using lean.nvim. If that is the case you can figure out how to type a character by hovering it in a Lean file and executing LeanAbbreviationsReverseLookup

image.png

[mars0i]

Thank you @Henrik Böving ! That's what I needed.

[François G. Dorais]

Kind of off topic but I always thought that using the middle dot · (U+0087) instead of the bullet • (U+2022) was an unusual choice for focusing on a goal in tactic mode.

[Eric Wieser]

The bullet is used heavily in mathlib, so I think that would be annoying from our side