Zulip Chat Archive

Stream: new members

Topic: List of Unicode Input Terms?


view this post on Zulip Toby Donaldson (Oct 04 2019 at 06:37):

Is there a complete list anywhere that shows all the \-terms for entering Unicode symbols? I mean things like \a, \lam, \to, etc. that could be used in VS Code.

view this post on Zulip Johan Commelin (Oct 04 2019 at 06:50):

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

view this post on Zulip Johan Commelin (Oct 04 2019 at 06:51):

We should probably link to this file from some visible places...

view this post on Zulip Johan Commelin (Oct 04 2019 at 06:51):

@Toby Donaldson :up:

view this post on Zulip Sebastien Gouezel (Oct 04 2019 at 07:07):

Do you know how is it possible to add something to this list (for instance \k for 𝕜, that showed up a lot lately)?

view this post on Zulip Johan Commelin (Oct 04 2019 at 07:10):

Yes, you just make a PR

view this post on Zulip Johan Commelin (Oct 04 2019 at 07:10):

And then ask Gabriel Ebner to merge it


Last updated: May 15 2021 at 02:11 UTC