Zulip Chat Archive

Stream: lean4

Topic: Tokens

Sébastien Gouëzel (Jul 15 2025 at 10:33):

I just noticed that 𝐜 (type with \bfc in vscode) is not an allowed token, while 𝕔 (type with \bbc) is. Is there a rationale behind this? Or could we add the bf letters to the list of tokens?

Last updated: Dec 20 2025 at 21:32 UTC