Stream: new members
Edward Ayers (Aug 07 2018 at 20:19):
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 (Aug 07 2018 at 20:22):
Edward Ayers (Aug 07 2018 at 20:22):
Gabriel Ebner (Aug 07 2018 at 20:45):
Also try out hovering over a Unicode character. Vscode will then show a popup that explains how to typee it.
Patrick Massot (Aug 07 2018 at 21:37):
Still, I think this file should be more visible somehow
Johan Commelin (Aug 08 2018 at 04:48):
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.
Last updated: May 15 2021 at 23:13 UTC