Why doesn't typing "\8" produce ₈ in VS Code?

Stream: new members

[Isak Colboubrani]

In VS Code (with the Lean extension), typing "\0" produces ₀, "\1" produces ₁, and so on.

However, typing "\8" does not produce ₈ as expected. Instead, you can type "\8 " (with a space, other characters may work too) to get the subscript ₈.

Why is ₈ different from the other subscript digits ₀₁₂₃₄₅₆₇₉ in this regard?

[Edward van de Meent]

this likely has to do with there being a different command which starts with 8?

[Julian Berman]

This will happen if the prefix is not unique. You'll see for 8 that there's an 8<:

https://github.com/leanprover/vscode-lean4/blob/master/lean4-unicode-input/src/abbreviations.json#L582

[Julian Berman]

You don't need to type the space, you can either hit tab to immediately make the replacement (without adding a space), or you can simply ignore that it stays looking like \8, if you keep typing and you don't type < as your next abbreviation it will eventually get replaced.

[Julian Berman]

That scissors abbreviation seems overly cute though. And I doubt it's used anywhere? Let's see.

[Julian Berman]

Yeah nowhere in Mathlib.

[Isak Colboubrani]

Heh, it seems like the demand for scissors is... low.

% cd mathlib4/
% git grep ✂
% cd ../lean4/
% git grep ✂
%

[Jz Pan]

Is ✂ even a valid character in identifier names?

[Jz Pan]

def ✂ := 42

mathlib-demo.lean:1:6
expected token

[Jz Pan]

Seems no.

[Edward van de Meent]

is it maybe a remnant from earlier lean/mathlib versions? or maybe this is a result of the list of shortcuts (hah) being copy-pasted from some unrelated place?

[Julian Berman]

Probably the latter would be my guess. Or someone really wants to be cute when adding notation for https://ncatlab.org/nlab/show/scissors+congruence (/s)

[Julian Berman]

(I looked in Julia and LaTeX and neither have that shortcut though)

[Markus Himmel]

I may have some of this wrong, but it looks to me like the following:

• The Unicode replacement feature of the Lean VS Code extension inherited its list of abbreviations from a now-defunct VS Code extension called Input Assist (in 2016)
• Input assist took its abbreviations from the Agda emacs mode
• The Agda emacs mode has contained the abbreviation since its first commit in 2008. The commit message says that most abbreviations are taken from the Emacs TeX input method, but I cannot find any evidence that the TeX input method had an abbreviation for the scissors in 2008 (or at any other point).

So it appears to me that the scissors were introduced by Nils Anders Danielsson for Agda, and in fact if you search GitHub for ✂ lang:Agda you will find a handful of uses of the scissors in Agda projects.

[Edward van de Meent]

Now that's some detective work!

[Mario Carneiro]

Jz Pan said:

Is ✂ even a valid character in identifier names?

That's the wrong question. Most unicode characters are not valid identifier characters, but any character can be used in notations. Certainly something like this would be used as a notation and not part of a name.