Zulip Chat Archive

Stream: general

Topic: VSCode unicode characters


view this post on Zulip 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": "ℤ√",

view this post on Zulip 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": "⁆",

?

view this post on Zulip Patrick Massot (Feb 10 2020 at 20:35):

"nhds" : "𝒩"

view this post on Zulip Patrick Massot (Feb 10 2020 at 20:56):

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

view this post on Zulip 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.

view this post on Zulip Floris van Doorn (Feb 10 2020 at 22:17):

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)?

view this post on Zulip 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 𝓝.

view this post on Zulip Gabriel Ebner (Feb 10 2020 at 22:20):

Can you also add ∃ᶠ?

view this post on Zulip Floris van Doorn (Feb 10 2020 at 22:25):

added "exf": "∃ᶠ",

view this post on Zulip Yury G. Kudryashov (Feb 10 2020 at 23:11):

Any chance to sync changes to emacs lean-mode?

view this post on Zulip Floris van Doorn (Feb 10 2020 at 23:49):

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

view this post on Zulip Mario Carneiro (Feb 10 2020 at 23:54):

I hope 𝓝 is already available as \calN

view this post on Zulip Mario Carneiro (Feb 10 2020 at 23:54):

or is it \scrN?

view this post on Zulip Yury G. Kudryashov (Feb 11 2020 at 00:08):

It's \MCN

view this post on Zulip Yury G. Kudryashov (Feb 11 2020 at 00:09):

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

view this post on Zulip Yury G. Kudryashov (Feb 11 2020 at 00:10):

E.g., 𝕜, ⥤

view this post on Zulip Mario Carneiro (Feb 11 2020 at 00:51):

what's the rationale for \MCN?

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Feb 11 2020 at 00:52):

I would prefer that to ad hoc things like \nhds

view this post on Zulip Mario Carneiro (Feb 11 2020 at 00:53):

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

view this post on Zulip Yury G. Kudryashov (Feb 11 2020 at 00:55):

math cal N

view this post on Zulip 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.

view this post on Zulip 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}

view this post on Zulip Mario Carneiro (Feb 11 2020 at 02:30):

and typing braces in vscode shortcut symbols is problematic

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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"

view this post on Zulip Mario Carneiro (Feb 11 2020 at 03:22):

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

view this post on Zulip Mario Carneiro (Feb 11 2020 at 03:22):

but many symbols also have shorter names for quicker typing

view this post on Zulip 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.

view this post on Zulip 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"

view this post on Zulip 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:

view this post on Zulip 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 →₁ₛ.

view this post on Zulip Mario Carneiro (Feb 11 2020 at 16:09):

in what sense is 𝓝 a multi character abbreviation?

view this post on Zulip 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

view this post on Zulip 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!

view this post on Zulip Floris van Doorn (Feb 11 2020 at 20:09):

Any chance to sync changes to emacs lean-mode?

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

view this post on Zulip 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).

view this post on Zulip Floris van Doorn (Feb 17 2020 at 01:35):

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.

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (May 13 2020 at 11:57):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Billy Price (May 13 2020 at 13:55):

Done.


Last updated: May 12 2021 at 05:19 UTC