VSCode unicode characters

Stream: general

[Floris van Doorn]

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]

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

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

?

[Patrick Massot]

"nhds" : "𝒩"

[Patrick Massot]

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

[Patrick Massot]

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]

I'm adding

    "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]

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

[Gabriel Ebner]

Can you also add ∃ᶠ?

[Floris van Doorn]

added "exf": "∃ᶠ",

[Yury G. Kudryashov]

Any chance to sync changes to emacs lean-mode?

[Floris van Doorn]

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

[Mario Carneiro]

I hope 𝓝 is already available as \calN

[Mario Carneiro]

or is it \scrN?

[Yury G. Kudryashov]

It's \MCN

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

E.g., 𝕜, ⥤

[Mario Carneiro]

what's the rationale for \MCN?

[Mario Carneiro]

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

[Mario Carneiro]

I would prefer that to ad hoc things like \nhds

[Mario Carneiro]

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

[Yury G. Kudryashov]

math cal N

[Tim Daly]

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]

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

[Mario Carneiro]

and typing braces in vscode shortcut symbols is problematic

[Tim Daly]

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]

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]

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]

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

[Mario Carneiro]

but many symbols also have shorter names for quicker typing

[Yury G. Kudryashov]

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

[Jesse Michael Han]

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]

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]

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

[Mario Carneiro]

in what sense is 𝓝 a multi character abbreviation?

[Gabriel Ebner]

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]

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]

Any chance to sync changes to emacs lean-mode?

Done: https://github.com/leanprover/lean-mode/pull/22

[Patrick Massot]

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]

I added

    "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]

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]

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

[Shing Tak Lam]

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]

@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]

Done.