https://github.com/leanprover/vscode-lean/pull/285

Stream: PR reviews

[Gabriel Ebner]

Add \specializes → ⤳ abbreviation

Everybody happy with the name?

[Johan Commelin]

I'm very happy with the name. I don't know if we want more names...

[Johan Commelin]

\∼>?

[Gabriel Ebner]

I'm not sure if that's easier to type than \spec.

[Yaël Dillies]

It is for me, but I have ~ on my AZERTY keyboard.

[Alex J. Best]

We already have ↝ (as \leadsto same as latex) which isn't used in mathlib, why not use that instead? (and maybe make \~> a synonym of that arrow).
For comparison : ↝ ⤳

[Gabriel Ebner]

cc @Andrew Yang

[Andrew Yang]

I think x ⤳ y looks better than x ↝ y. But I suppose it would be better to stick with existing ones?

[Alex J. Best]

Yeah the new one is bigger and nicer looking in my vscode too, what do you think about switching to the new symbol but keeping the latex \leadsto synonym then, rather than having two quite similar wavy arrows

[Gabriel Ebner]

But I suppose it would be better to stick with existing ones?

It's a bit less effort if we don't need to add a new abbreviation, but that shouldn't be the deciding factor. Looking better and not clashing with potential notation for convergence are stronger reasons.

[Gabriel Ebner]

I'm not really in favor of renaming existing abbreviations, in particular if the semantic mnemonic no longer matches the new use.

[Andrew Yang]

Sure. In this case, I think I'll stick with ⤳ and use the abbreviation \specializes and \~>.