Unicode input for →ₛₗ

Stream: lean4

[Anthony Fernandes]

It seems that the vscode extension doesn't have an abbreviation for →ₛₗ.

Following the examples of →ₗand →ₛ, I suggest to add rsl, tosl, r_sl, to_sl and semilinearmap as abbreviations for →ₛₗ. PR here

[Aaron Liu]

I thought we were all just supposed to do \r\_s\_l

[Aaron Liu]

what's the abbreviations for →ₗand →ₛ?

[Eric Wieser]

\tol is one of the

[Anthony Fernandes]

→ₗ has rl, tol, r_l, to_l and linearmap

→ₛ has rs, tos, r_s, to_s and simplefunc

[Jireh Loreaux]

I can't believe we have that for simple functions. That's not even scoped notation, it's only local!

[Marc Huisinga]

Is there consensus that these shortcuts are common enough that they should be added?

[Floris van Doorn]

Personally I think that all multi-character scoped and global notation in Mathlib deserves a dedicated shortcut.

[Floris van Doorn]

These multi-character shortcuts are not very discoverable (is there a better way than navigating abbreviations.json?)
Should we add the keyboard shortcuts to the docstring of multi-character notations?
Oh wait, these shortcuts now show up in the tooltip of the first character. Nice!

[Marc Huisinga]

Floris van Doorn said:

These multi-character shortcuts are not very discoverable (is there a better way than navigating abbreviations.json?)

We also have a built-in table view of abbreviations.json that you can find under Forall menu > Documentation > Show Unicode Input Abbreviations