how to write a superscript quickly?

Stream: new members

[Chris M]

I want to write a^{-1}. How do I do this in lean?

[Shing Tak Lam]

\inv

[Chris M]

cool

[Johan Commelin]

Also \-1

[Scott Morrison]

Also -- if you hover the mouse over any symbol in VSCode, the tooltip will tell you how to type it.

[Eric Wieser]

Is there a reason vscode has no methanism to type ᵥ?

[Johan Commelin]

Probably because nobody wrote a PR that adds it to translations.json

[Eric Wieser]

Mind linking to that file on github?

[Shing Tak Lam]

https://github.com/leanprover/vscode-lean/blob/master/translations.json (I think)

[Eric Wieser]

It also puzzles me that \_ produces ₐ (\_a)

[Eric Wieser]

Thanks @Shing Tak Lam. Looks like @Utensil Song beat me to it: https://github.com/leanprover/vscode-lean/blame/670606ba0ab2ae668b431169aa81e8f77b1c2d78/translations.json#L1284

[Mario Carneiro]

When you write a prefix of a valid shortcut it uses the first one that matches

[Eric Wieser]

Would it be reasonable to do that only if there are not multiple tied shortest ones?

[Mario Carneiro]

why? It's still better than nothing

[Mario Carneiro]

and you can train your muscle memory to it regardless of how weird it is

[Eric Wieser]

Until someone adds a new shortcut that happens to be the same length as an existing one but alphabetically sooner

[Eric Wieser]

And then the muscle memory breaks

[Mario Carneiro]

sure, which is why changes to translations.json shouldn't be taken lightly

[Mario Carneiro]

in most common cases we also have duplicates for prefixes when we want to calibrate this behavior

[Mario Carneiro]

but I think if the file was closed under taking prefixes it would be about 200-300% larger

[Eric Wieser]

Just for context for anyone else reading, these are the lines in question that I'm worried about

https://github.com/leanprover/vscode-lean/blob/66952a2fd27b3821ef4f67ad4b55e99f6a3991ab/src/input.ts#L262-L267

[Mario Carneiro]

Looking at that code, it's also deterministic based on the order they appear in the file

[Mario Carneiro]

so you can calibrate preferences by reordering too

[Eric Wieser]

I'm not certain that's true - from what I can tell, keys that look like numbers are shuffled, at least in some javascript implementations

[Mario Carneiro]

I don't think that's a major issue since the only keys that look like numbers are \0 ...\9 which have no proper prefixes

[Mario Carneiro]

you might be right though if this is stored as a hashmap

[Mario Carneiro]

Anyway, the way I would look at it is that \_ is unassigned, so by luck it currently resolves to \_a. If that's what you wanted, great, otherwise maybe say what you mean or come up with something better that \_ should resolve to

[Eric Wieser]

What bugs me is I normally type \_ by accident due to hitting space too soon or something, and having it complete as a makes me squint to work out what happened.

[Mario Carneiro]

generally whenever you write \... it will complete to a character if and only if you write a space. If you didn't finish writing the sequence you wanted then you probably got the wrong character

[Mario Carneiro]

if you learn the shortest sequence then that's basically true by definition

[Mario Carneiro]

If the issue is that you don't realize that you typed \_a instead of \_v and can't see the difference between the characters, then that's probably overuse of unicode or a bad font

[Eric Wieser]

That's a fair comment

[Eric Wieser]

One thing I'd perhaps propose is to allow blacklisting sequences as "_": null, in that file. If the shortest sequence matches a blacklisted one, then perform no replacement.

[Eric Wieser]

But essentially I'm describing damage control for my own clumsy typing...

[Mario Carneiro]

An easy way to accomplish that would be "_": "\_"

[Mario Carneiro]

It would be nice if users could add their own translations via vscode settings

[Mario Carneiro]

maybe they already can, I'm not sure

[Eric Wieser]

Allowing customization sounds hard given we just decided they were ordered

[Eric Wieser]

Your approach feels like a (effective) hack, changing the typescript to allow null would be fairly trivial

[Mario Carneiro]

On startup it would read the settings and overwrite all the global translations as directed

[Mario Carneiro]

I don't deny it is a hack

[Eric Wieser]

Ah, so tell users to start by copying the entire translations.json, rather than attempting to merge user translation settings with upstream ones

[Mario Carneiro]

If you want to support that in vscode, PR's are welcome

[Mario Carneiro]

No, I'm saying merge settings

[Eric Wieser]

Just thought I'd float the idea before bothering with a PR. If it keeps bugging me, I'll make one :)

[Mario Carneiro]

like if translations.json has {"a": "A", "b": "B", "d": "D"} and settings.json has "lean.translations_override": {"a": "C", "b": null, "c": "C"} then it behaves as though it was given {"a": "C", "b": null, "c": "C", "d": "D"}

[Mario Carneiro]

so if the underscore thing bothers you then you can add {"_": null} to your local settings and translations.json doesn't have to change

[Mario Carneiro]

and you still get the benefit of future changes to translations.json

[Eric Wieser]

How does your merger decide at what position to insert c?

[Edward Ayers]

This already exists in vscode: eg

    "lean.input.customTranslations": {
        "a": "α",
        "al": "α", "be": "β", "ga": "γ", "de": "δ", "ep": "ε", "ze": "ζ",
        "et": "η", "th": "θ", "io": "ι", "ka": "κ", "la": "λ", "mu": "μ",
        "nu": "ν", "xi": "ξ", "pi": "π", "rh": "ρ", "si": "σ",
        "ta": "τ", "ph": "φ", "ch": "χ", "ps": "ψ", "om": "ω",
    ...
    }

[Edward Ayers]

then vscode will merge the translation files, with the ones in customTranslations clobbering the other

[Edward Ayers]

although there is no null support as of yet

[Eric Wieser]

To be clear with my point about clobbering - javascript objects are ordered dictionaries, so there's not a unique definition of what merging looks like

[Edward Ayers]

I think in the sourcecode it is just {...globalTranslations, ...customTranslations}, so they are treated as unordered here.

[Eric Wieser]

That results in the order being (assuming VScode matches chrome):

• Existing keys keep their order
• custom keys are added last (so will never win ties)

[Eric Wieser]

Edward Ayers said:

although there is no null support as of yet

Reading the source, it looks like it is implicitly already supported.

[Edward Ayers]

No custom keys always win ties.

[Eric Wieser]

{...{d: 1, c:2, b:3}, ...{c:3, a:5}} results in {d: 1, c: 3, b: 3, a: 5} with the key a being last. The lines I link to above show the earliest element is used to break ties.

[Edward Ayers]

I believe Javascript objects are unordered dictionaries so it doesn't matter where a appears in the resulting object. The important thing is that in your example c:3 clobbers c:2 .

[Eric Wieser]

If that were true there would be bigger problems for breaking ties, since the completer is affected by their iteration order.

[Edward Ayers]

Ah I see what you mean, in the case that the string is not an exact match it iterates through the object so the iteration order matters. In the implementation, it takes the shortest completion so there is only iteration-order-dependence if there are two completions with the same length and the same prefix.

[Eric Wieser]

Yes, and that case is what this conversation started as :)

[Mario Carneiro]

But if you add your own custom translation for a prefix then you don't have to worry about tiebreak behavior

[Edward Ayers]

Custom translations supports null with this PR: https://github.com/leanprover/vscode-lean/pull/197