Zulip Chat Archive

Stream: new members

Topic: List of Unicode Input Terms?


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.

Johan Commelin (Oct 04 2019 at 06:50):

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

Johan Commelin (Oct 04 2019 at 06:51):

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

Johan Commelin (Oct 04 2019 at 06:51):

@Toby Donaldson :up:

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)?

Johan Commelin (Oct 04 2019 at 07:10):

Yes, you just make a PR

Johan Commelin (Oct 04 2019 at 07:10):

And then ask Gabriel Ebner to merge it


Last updated: Dec 20 2023 at 11:08 UTC