0
$\begingroup$

When reading mathematics books, there are often different fonts for indicating concepts such as sets and algebraic structures. In Lean 4 using VSCode:

\bn produces the unicode ℕ representing natural numbers.

\bC produces ℂ representing complex numbers.

(but it's not complete. e.g. \bx does not produce a similar font).

The question is:

Are there other escape sequences that systematically generate different mathematical fonts?

If not, how to enter them in Lean 4?

-- Update --

I understand that this is a VSCode mechanism (for entering math symbols therein). And I have now added a vscode tag. But my question is whether there are some rules in those escape sequences. For example, In addition to \bn, \bc etc., there is also

\MCP   for 𝓟
\MCC   for 𝓒

etc.

What I am asking is whether there are known rules in naming these escape sequences (specifically for the math types). Or does one have to enumerate via "Lean 4: Docs: Show Unicode Input Abbreviations", and reverse engineer to figure out?

Improve this question
$\endgroup$
3
  • $\begingroup$ I think this is already answered somewhere on this site. (I can try to find it tomorrow.) It is just a hard coded list of symbols for the vs code plugin that also are now used for other editor plugins. There aren’t really “fonts” or “font styles” that I’m aware of. $\endgroup$
    – Jason Rute
    Commented Nov 16 at 5:37
  • 1
    $\begingroup$ I don't understand what you're asking. Someone came up with a bunch of mnemonics, roughly based on LaTeX and visual cues (such as \-> and \u=). What do you expect beyond this? $\endgroup$
    – Andrej Bauer
    Commented Nov 17 at 19:52
  • $\begingroup$ They are all hard coded, not systematic $\endgroup$
    – ice1000 ♦
    Commented Nov 24 at 13:13

3 Answers 3

Reset to default
4
$\begingroup$

Lean 4 accepts any UTF8 symbols. UTF8 is not a font but a coding standard for characters. Various fonts contain various symbols and none contains all. Anyhow, entering these symbols and using appropriate fonts is a task for Visual Studio Code, not Lean itself.

When working in Visual Studio Code in a Lean file, you may run the command Lean 4: Docs: Show Unicode Input Abbreviations, which you do by pressing Ctrl+Shift+P (on Mac it is Cmd+Shift+P) and start typing "abbreviation" until you see the command. There is no need to rummage through source code.

Improve this answer
$\endgroup$
2
$\begingroup$

Thanks to the two prior answers for pointing out that this is a feature of the VS Code lean extension. I went through the list in "Lean 4: Docs: Show Unicode Input Abbreviations", and it seems that there is indeed a regular pattern for entering the Unicode of different styles of English characters, as is demonstrated in the following table (using only the first letter A as an example):

\bfA  𝐀
\bfa  𝐚
\MiA  𝐴
\Mia  𝑎
\MIA  𝑨
\MIa  𝒂
\McA  𝒜
\Mca  𝒶
\MCA  𝓐
\MCa  𝒶
\MfA  𝔄
\Mfa  𝔞
\bbA  𝔸
\bba  𝕒

There are shortcuts such as \bn (same as \bbN ℕ) for some but not all of the letters.

Improve this answer
$\endgroup$
1
$\begingroup$

This is not a feature of Lean per se but of the Lean VSCode extension.

The full list of symbols can be found here in the source code.

The extension does not set a different font, rather, it helps with inputting different Unicode characters. If you open the file with another editor, you will see the ℕ still rendered as ℕ and not as N, because it's not N in a different font, but the character U+2115 DOUBLE-STRUCK CAPITAL N (just like ï is not “i in a different font”). Alternative ways to input these characters include extensions in other editors, copy-pasting, math keyboards, and Compose key sequences.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.