How to type calligraphic characters

Stream: new members

[Rémy Degenne]

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 ?

[Johan Commelin]

yup translations.json in the vscode-lean repo

[Johan Commelin]

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

[Rémy Degenne]

Thanks!

[Johan Commelin]

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

[Bryan Gin-ge Chen]

I'm not a Zulip admin unfortunately.

[Bryan Gin-ge Chen]

How's this? #translations

[Patrick Massot]

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.