VSCode abbreviation for ↦

Stream: general

[Michael Stoll]

Currently in VSCode, \m → μ, \ma → ♂, \map → ↦, which tends to be very annoying when I mistype (and needs four keystrokes to produce ↦). I need ↦ all the time, μ only on very rare occasions and ♂ never. Can I propose to change the behavior of the Lean extension so that \m → ↦, \mu → μ, and\ma → ♂ instead?

[Eric Rodriguez]

I don't think we need \male at all, do we?

[Michael Stoll]

Who knows what it might be useful for in the future...

[Ruben Van de Velde]

=> is only two keystrokes :)

[Yury G. Kudryashov]

Ruben Van de Velde said:

=> is only two keystrokes :)

What exactly do you suggest: don't use ↦ or something else?

[Kyle Miller]

Is there a way to make \ma prefer ↦ over ♂? I assume there must be, given that it's preferring ♂ at the moment.

[Kevin Buzzard]

It really frustrates me that I can't use \mapsto in some cases and I'm forced to use => (which my students never otherwise see)

[Patrick Massot]

Getting \male out of the way is really easy and uncontroversial I think.

[Michael Stoll]

Kevin Buzzard said:

It really frustrates me that I can't use \mapsto in some cases and I'm forced to use => (which my students never otherwise see)

That's a different problem, though.

[Patrick Massot]

I think making the full abbreviation longer than mapsto is enough. Something like \malesymbol.

[Michael Stoll]

I woud still argue that \m should not give μ, but ↦. This must be possible, I assume.

[Eric Rodriguez]

While we're constructing the bikeshed, I'd like to add \hookrightarrow - iirc you need to type \hookr for that to show up

[Mario Carneiro]

One easy way to improve this kind of thing would be to have the abbreviations.json file be order dependent and prefer earlier entries, and then sort it by number of occurrences in mathlib (or at least use this to find suggestions for pairs that should be reordered)

[Mario Carneiro]

I'm not sure if it's a good or bad thing that this list is derived from some latex listing rather than only being organically grown from user requests. The good thing is that if you pick a new symbol it is often the case that it already has an abbreviation and you don't need to petition to add one, but the bad thing is that sometimes the weird symbols beat out the actually useful ones

[Mario Carneiro]

I think mapsto has some other abbreviations too, like \|->, but that's a bit too many punctuation characters to type comfortably

[Mario Carneiro]

what about co-opting \=>?

[Michael Stoll]

... and even so, it is still four keystrokes.

[Michael Stoll]

(or three, for \=>.)

[Mario Carneiro]

or \m>

[Mario Carneiro]

\|> is also unused

[Michael Stoll]

What is the problem with just \m? I bet ↦ is the most frequently used symbol whose abbreviation starts with "m".

[Mario Carneiro]

I think it is more mnemonic to have the greek letters on single letters

[Michael Stoll]

Note that \d gives ↓ already.

[Mario Carneiro]

although we already have several divergences for this for \d, \l, \n

[Mario Carneiro]

TBH I think \d is useless and that should be delta

[Michael Stoll]

and \i gives ∩, so it does not look like this is a rule.

[Michael Stoll]

also \l and \r give arrows.

[Mario Carneiro]

I think many of them are just being hit by the whims of the random selection algorithm we're seeing here for \ma

[Michael Stoll]

and \t and \u...

[Mario Carneiro]

e.g. I doubt \d is actually assigned to ↓, it's just the first one the algorithm happens to pick

[Michael Stoll]

I like your idea to give the shorter abbreviations to the symbols used more frequently in Mathlib.

[Mario Carneiro]

actually I take it back, \u \d \l \r look like they are deliberate when considered as a group

[Mario Carneiro]

I have to be careful with typing delta too, \D is Delta but \De is Ϯ <- whatever that is

[Mario Carneiro]

\M is 𝐴...?

[Mario Carneiro]

we should really go through and properly huffman code these things

[Mario Carneiro]

I think it would also be a good idea to require the list of abbreviations to be a meet-semilattice under the longest common prefix operation, so that the algorithm doesn't have to pick (and invariably pick badly)

[Ruben Van de Velde]

Is sub still subset while subs is strict subset?

[Michael Stoll]

\su and \sub give ⊆, \subs gives ⊂.

[Max Nowak 🐉]

This feels like it should have some sensible defaults, but otherwise be customizable per user in their vscode config.

[Eric Rodriguez]

For subsets I think \ss can be used

[Eric Wieser]

Max Nowak 🐉 said:

This feels like it should have some sensible defaults, but otherwise be customizable per user in their vscode config.

These abbreviations are already customizable, I believe

[Gabriel Ebner]

Kyle Miller said:

Is there a way to make \ma prefer ↦ over ♂? I assume there must be, given that it's preferring ♂ at the moment.

IIRC the trick was to add a "ma": "↦", line.

[Mario Carneiro]

hence the suggestion:

Mario Carneiro said:

I think it would also be a good idea to require the list of abbreviations to be a meet-semilattice under the longest common prefix operation, so that the algorithm doesn't have to pick (and invariably pick badly)