completions

Stream: new members

[Edward Ayers]

Hi gang where can I get a list of available completions for lean? Eg \all -> forall symbol etc. vscode doesn't give me a list when I type \. Also what is the best way to ask questions that have likely come up before?

[Patrick Massot]

https://github.com/leanprover/vscode-lean/blob/master/translations.json

[Edward Ayers]

thanks

[Gabriel Ebner]

Also try out hovering over a Unicode character. Vscode will then show a popup that explains how to typee it.

[Patrick Massot]

Still, I think this file should be more visible somehow

[Johan Commelin]

Maybe the popup could show a link to the translations file? If it is an actual hyperlink, then you don't even have to typeset the entire URL, so it wouldn't even take up much space.