## Stream: general

### Topic: VSCode unicode characters

#### Floris van Doorn (Feb 10 2020 at 20:15):

Are there any (combinations of) unicode characters you wish to input in a shorter/different way? Put requests in this thread! I'm currently making a PR to vscode-lean with already some additions, in the list below: (for example the first entry means that if you type \allf you get ∀ᶠ)

    "allf": "∀ᶠ",
"all^f": "∀ᶠ",
"allm": "∀ₘ",
"all_m": "∀ₘ",
"to0": "→₀",
"r0": "→₀",
"to_0": "→₀",
"r_0": "→₀",
"finsupp": "→₀",
"to1": "→₁",
"r1": "→₁",
"to_1": "→₁",
"r_1": "→₁",
"l1": "→₁",
"to1s": "→₁ₛ",
"r1s": "→₁ₛ",
"to_1s": "→₁ₛ",
"r_1s": "→₁ₛ",
"l1simplefunc": "→₁ₛ",
"toa": "→ₐ",
"ra": "→ₐ",
"to_a": "→ₐ",
"r_a": "→ₐ",
"alghom": "→ₐ",
"tob": "→ᵇ",
"rb": "→ᵇ",
"to^b": "→ᵇ",
"r^b": "→ᵇ",
"boundedcontinuous": "→ᵇ",
"tol": "→ₗ",
"rl": "→ₗ",
"to_l": "→ₗ",
"r_l": "→ₗ",
"linearmap": "→ₗ",
"tom": "→ₘ",
"rm": "→ₘ",
"to_m": "→ₘ",
"r_m": "→ₘ",
"aeeqfun": "→ₘ",
"rp": "→ₚ",
"to_p": "→ₚ",
"r_p": "→ₚ",
"dfinsupp": "→ₚ",
"tos": "→ₛ",
"rs": "→ₛ",
"to_s": "→ₛ",
"r_s": "→ₛ",
"simplefunc": "→ₛ",
"root": "√",
"sqrt": "√",
"boxmid": "◫",
"hcomp": "◫",
"Pi0": "Π₀",
"P0": "Π₀",
"Pi_0": "Π₀",
"P_0": "Π₀",
"Rge0": "ℝ≥0",
"R>=0": "ℝ≥0",
"nnreal": "ℝ≥0",
"Zsqrt": "ℤ√",
"zsqrtd": "ℤ√",


#### Oliver Nash (Feb 10 2020 at 20:33):

Oh cool! I would quite like something shorter for ⁅ and ⁆ (currently textlquill and textrquill). Maybe:

    "liel": "⁅",
"lier": "⁆",


?

#### Patrick Massot (Feb 10 2020 at 20:35):

"nhds" : "𝒩"

#### Patrick Massot (Feb 10 2020 at 20:56):

I also vote for getting back "X":"⨯", that was accidentally removed by Ed.

#### Patrick Massot (Feb 10 2020 at 20:58):

If a superscript f now officially means filter (at least if the some localized notation is opened) then I would also like "xf" : "×ᶠ" which would become notation for filter product.

#### Floris van Doorn (Feb 10 2020 at 22:17):

    "liel": "⁅",
"bracketl": "⁅",
"lier": "⁆",
"bracketr": "⁆",
"nhds": "𝓝",
"nbhds": "𝓝",
"X": "×",
"vectorproduct": "⨯",
"crossproduct": "⨯",
"coprod": "⨿",
"sigmaobj": "∐",
"bigcoprod": "∐",
"xf": "×ᶠ",


@Patrick Massot: I fixed the 𝓝 to mean the actual character used in mathlib. For "X", I think you mean the same unicode character as for \x (× multiplication sign, used all over mathlib) instead of the one you wrote (⨯ vector or cross product, only used in 1 category theory file)?

#### Floris van Doorn (Feb 10 2020 at 22:18):

Note: for the long names, any prefix (that is unambiguous) will also work. So for example \nhd should also give 𝓝.

#### Gabriel Ebner (Feb 10 2020 at 22:20):

Can you also add ∃ᶠ?

#### Floris van Doorn (Feb 10 2020 at 22:25):

added "exf": "∃ᶠ",

#### Yury G. Kudryashov (Feb 10 2020 at 23:11):

Any chance to sync changes to emacs lean-mode?

#### Floris van Doorn (Feb 10 2020 at 23:49):

I'll add these changes to the Emacs lean-mode as well.

#### Mario Carneiro (Feb 10 2020 at 23:54):

I hope 𝓝 is already available as \calN

#### Mario Carneiro (Feb 10 2020 at 23:54):

or is it \scrN?

It's \MCN

#### Yury G. Kudryashov (Feb 11 2020 at 00:09):

Some other characters are missing but I have them in my ~/.XCompose.

E.g., 𝕜, ⥤

#### Mario Carneiro (Feb 11 2020 at 00:51):

what's the rationale for \MCN?

#### Mario Carneiro (Feb 11 2020 at 00:52):

I think it should be easy to add the complete unicode blocks for script, double struck, and other "font variant" math symbols

#### Mario Carneiro (Feb 11 2020 at 00:52):

I would prefer that to ad hoc things like \nhds

#### Mario Carneiro (Feb 11 2020 at 00:53):

(although we can have that short cut too if people use it)

math cal N

#### Tim Daly (Feb 11 2020 at 02:28):

Hmmm... wouldn't it make sense to use the Latex names for the symbols? That way you could use the Latex documentation to look up symbols you want and they would be compatible with other documentation.

#### Mario Carneiro (Feb 11 2020 at 02:29):

the latex name is especially inconvenient here because it's not just a name, it is \mathcal{N}

#### Mario Carneiro (Feb 11 2020 at 02:30):

and typing braces in vscode shortcut symbols is problematic

#### Tim Daly (Feb 11 2020 at 02:32):

I agree with Z, C,N, etc. But, again, it comes down to using existing naming conventions or inventing local ones. It adds a layer of pain when my proofs need to be "translated" at the level of basic syntax. And if the table is designed to be "extensible", then when I want a special glyph (e.g. \leadsto) I can insert it.

#### Tim Daly (Feb 11 2020 at 02:34):

Most mathematicians already know the names of glyphs in their area. Having to look up alternate names just makes the learning curve steeper.

#### Tim Daly (Feb 11 2020 at 02:46):

It also has the advantage that @Jeremy Avigad natural language version of a theorem has a (math-speak) translation, so if one is doing operational semantics then the \leadsto glyph is naturally translated to "leads to"

#### Mario Carneiro (Feb 11 2020 at 03:22):

the names of most symbols are already based very obviously on the latex names

#### Mario Carneiro (Feb 11 2020 at 03:22):

but many symbols also have shorter names for quicker typing

#### Yury G. Kudryashov (Feb 11 2020 at 03:37):

There are many tables with unicode->latex translation. No need to have one more in lean-mode / vscode plugin.

#### Jesse Michael Han (Feb 11 2020 at 08:27):

what's the rationale for \MCN?

iirc \Mcn is mathcal and \MCN is mathscr, or something like that

i just think of them as "curly" and "extra-curly"

#### Gabriel Ebner (Feb 11 2020 at 10:13):

I would prefer that to ad hoc things like \nhds

Personally I much prefer semantic names like \nhds to random and hard to type strings like \MCN. But then I also write \land and \lor in LaTeX, and would definitely use \newcommand\nhds{\mathcal{N}}. :shrug:

#### Gabriel Ebner (Feb 11 2020 at 10:20):

BTW I also changed the abbreviation hover so that it also works if you hover over multi-character abbreviations like 𝓝 or →₁ₛ.

#### Mario Carneiro (Feb 11 2020 at 16:09):

in what sense is 𝓝 a multi character abbreviation?

#### Gabriel Ebner (Feb 11 2020 at 16:39):

The string 𝓝 is obviously composed of the two characters � and �. Or at least that's what javascript (and vscode) believe because they treat strings as lists of UTF-16 code units:

> '𝓝'.length
2


#### Floris van Doorn (Feb 11 2020 at 19:48):

BTW I also changed the abbreviation hover so that it also works if you hover over multi-character abbreviations like 𝓝 or →₁ₛ.

This is working great!

#### Floris van Doorn (Feb 11 2020 at 20:09):

Any chance to sync changes to emacs lean-mode?

#### Patrick Massot (Feb 16 2020 at 19:14):

Floris van Doorn said:

@**Patrick Massot|110031**: I fixed the 𝓝 to mean the actual  character used in mathlib. For "X", I think you mean the same unicode character as for \x (× multiplication sign, used all over mathlib) instead of the one you wrote (⨯ vector or cross product, only used in 1 category theory file)?


Crap, I missed that message (I found it today my reviewing recent mentions to make sure I didn't miss too many). The 𝓝was meant to be the one used in mathlib yes. But the cross definitely wasn't. We already have abbreviations for that one, I really meant ⨯ vector or cross product. I won't fight to get that one used in mathlib since the difference with × multiplication sign is hard to see, but it's really handy to be able to use it (and type it easily) for custom files (for instance I used it during talks).

#### Floris van Doorn (Feb 17 2020 at 01:35):

    "vectorproduct": "⨯",
"crossproduct": "⨯",


for the product you mentioned. It will already do the substitution on a prefix, if unambiguous, so \cro (and maybe \cr) will likely work. You can make a PR yourself also assigning it to \X.

#### Billy Price (May 13 2020 at 11:53):

I have two questions. Are all unicode characters allowed in lean? If not is there a good resource for viewing all of them? I have been using this https://github.com/leanprover/vscode-lean/blob/master/translations.json. Is that basically all of them or just some subset chosen because they are common/useful?

Other question is regarding multi-cursor input in VS Code. I almost constantly use cmd+D and cmd+option+downarrow to type with multiple cursors, for example, to quickly select and change some variable name - but this completely disables the backslash-unicode character entry. So if I want to change all the Gammas to Deltas, I would highlight them all by hitting cmd+D a bunch of times to highlight them all, but when I type \Delta and hit tab or space, it does not convert to unicode as it usually would. Any way to fix this - or another way of fast name changing?

#### Kevin Buzzard (May 13 2020 at 11:57):

I have independently noticed this multi-cursor input issue and would love to hear a solution.

#### Shing Tak Lam (May 13 2020 at 12:00):

Do you mean what is allowed as an identifer? If so, see this thread

Also the notation key word is flexible enough, and you can see some of the shenanigans I got up to using it in that thread. I think with notation almost anything is allowed.

#### Bryan Gin-ge Chen (May 13 2020 at 13:47):

@Billy Price Could you open the multi-cursor input question as an issue on the vscode-lean repo? It looks like a limitation of our unicode input system. I can't promise that anyone will fix it right away, but it's easier to track there than in a Zulip thread.

#### Billy Price (May 13 2020 at 13:55):

Done.

Last updated: May 12 2021 at 05:19 UTC