bold face N

Stream: general

[Kevin Buzzard]

In older mathematical textbooks, a bold face N was used to denote the natural numbers. I would like to make a bold face N in a game but I have no clue how to make that happen.

[Floris van Doorn]

Maybe 𝐍(U+1D40D)?

[Floris van Doorn]

Then you can just do

notation `𝐍` := mynat

There is no keyboard shortcut for 𝐍 in VSCode (yet), so that might be annoying...

[Daniel Fabian]

Let me suggest you make a bug / feature request on github about it. Most open source projects tend to respond fairly quickly to open issues. And since this is a trivial one, chances are someone would pick it up quickly.

[Shing Tak Lam]

The VSCode keyboard shortcut is done by the Lean extension, so it's easy for someone here to add it.

[Daniel Fabian]

sure, I'm just suggesting to collect the features on github, because presumably there are more than this single one around ;-)

[Utensil Song]

Does 𝑵( which is \MIN in VS Code ) work for you? @Kevin Buzzard

[Utensil Song]

You can also search "N" (which will be turned to a search of unicode variants of "N" in Chrome) in https://github.com/leanprover/vscode-lean/blob/master/translations.json and choose the one you like.

[Utensil Song]

One could create a PR following https://en.wikipedia.org/wiki/Mathematical_Alphanumeric_Symbols . (I can't do it atm, but will do when I can if no PRs created by then)

[Alex Peattie]

You can also add a custom Unicode shortcut in VS Code, like so:

• Open the Command Palette (⇧⌘P)
• Choose Preferences: Open Settings (JSON)
• Add:

"lean.input.customTranslations": {
  "boldn": "𝐍"
}

(before the closing }). Now you can input 𝐍 with \boldn

[Alex Peattie]

But I suppose if it's for a game that others will be playing a PR to vscode-lean might be better in the long-term :smile: . Also if the game is destined for an online version (i.e. like the natural numbers game), the Lean web editor has a separate set of Unicode abbreviations FYI (it might be an idea to consolidate into a single "source of truth" one day)

[Utensil Song]

(deleted)

[Utensil Song]

leanprover/vscode-lean#221