Zulip Chat Archive

Stream: new members

Topic: completions


view this post on Zulip 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?

view this post on Zulip Patrick Massot (Aug 07 2018 at 20:22):

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

view this post on Zulip Edward Ayers (Aug 07 2018 at 20:22):

thanks

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Aug 07 2018 at 21:37):

Still, I think this file should be more visible somehow

view this post on Zulip 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