Zulip Chat Archive

Stream: new members

Topic: How to type calligraphic characters


view this post on Zulip Rémy Degenne (Nov 06 2020 at 15:07):

Hello. Is there a list somewhere of all the commands used to type all sorts of characters? I just discovered by chance the \bb* commands to have the equivalent of the latex mathbb characters. Is there a way to get an equivalent of mathcal ?

view this post on Zulip Johan Commelin (Nov 06 2020 at 15:10):

yup translations.json in the vscode-lean repo

view this post on Zulip Johan Commelin (Nov 06 2020 at 15:11):

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

view this post on Zulip Rémy Degenne (Nov 06 2020 at 15:11):

Thanks!

view this post on Zulip Johan Commelin (Nov 06 2020 at 15:11):

@Bryan Gin-ge Chen @Jalex Stark @Rob Lewis can we have #translations point to that url?

view this post on Zulip Bryan Gin-ge Chen (Nov 06 2020 at 15:12):

I'm not a Zulip admin unfortunately.

view this post on Zulip Bryan Gin-ge Chen (Nov 06 2020 at 15:41):

How's this? #translations

view this post on Zulip Patrick Massot (Nov 06 2020 at 17:23):

We should also have a link from the community website somewhere. Actually I'm not even sure we have any link to the VSCode extension documentation on the website.


Last updated: May 14 2021 at 14:20 UTC