Zulip Chat Archive

Stream: new members

Topic: How to type calligraphic characters


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 ?

Johan Commelin (Nov 06 2020 at 15:10):

yup translations.json in the vscode-lean repo

Johan Commelin (Nov 06 2020 at 15:11):

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

Rémy Degenne (Nov 06 2020 at 15:11):

Thanks!

Johan Commelin (Nov 06 2020 at 15:11):

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

Bryan Gin-ge Chen (Nov 06 2020 at 15:12):

I'm not a Zulip admin unfortunately.

Bryan Gin-ge Chen (Nov 06 2020 at 15:41):

How's this? #translations

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: Dec 20 2023 at 11:08 UTC