Changing the abbreviation for `\n`

Stream: lean4

[Marc Huisinga]

A common UX issue for pretty much anyone using Lean for programming (including long-time Lean users) is that the \n abbreviation, which you type whenever you want to designate a newline, currently expands to ¬ by default. I myself get bitten by this most days when writing Lean. For programming purposes, it would be much nicer if it expanded directly to \n instead.
vscode-lean4#671 is a draft PR that proposes \n to expand to \n and also changes the abbreviation of \! to expand to ¬, so that there is still a single-character abbreviation for the symbol.
Even after this change, it will still be possible to set \n to expand to ¬ in the Lean 4 > Input: Custom Translations VS Code extension setting, and if desired Mathlib could even set this in its settings.json file for the whole project, since VS Code setting objects are merged, not overridden.

However, I appreciate that this may be quite a controversial change of a default, as surely most people doing theorem proving with Lean have so far built muscle-memory for \n to expand to ¬, and would now have to type \no, \not or \! instead or change the abbreviation in their VS Code settings. And on the other side of this is the currently confused muscle memory of anyone doing programming with Lean now and in the future :-)
I'd hence like to hear some thoughts on this by others. Does anyone have strong opinions on this proposed change?

Some prior discussions of this:
#new members > ✔ Unicode keybindings in VSCode
#lean4 > Keep VS Code from replacing escape sequence? @ 💬
(I'm sure there were other discussions in the past, but I can't find them because Zulip doesn't allow searching for \n or ¬, unfortunately)

[Bhavik Mehta]

I'm personally in favour of this change, since the \nhas annoyed me quite often in the past, and I think I use \notfor that symbol anyway. But I wonder if there's another solution here, such as a shortcut to easily and temporarily disable abbreviations. My reasoning for this is that similar issues to \noccur when writing latex for mathlib docs or for latex or html in verso, and changing all abbrevs like this seems hard to scale and more disruptive.

[Marc Huisinga]

Bhavik Mehta said:

But I wonder if there's another solution here, such as a shortcut to easily and temporarily disable abbreviations. My reasoning for this is that similar issues to \noccur when writing latex for mathlib docs or for latex or html in verso, and changing all abbrevs like this seems hard to scale and more disruptive.

I think this is orthogonal, since if you consciously realize "I need to disable abbreviations before typing this \n", you could also just type \\n instead. I can see that this might be more useful in the context of writing LaTeX docs for other abbreviations, though, so please create a GitHub issue in the vscode-lean4 repo for it :-)

[Bhavik Mehta]

Oh! I didn't think about that way of doing it. Yes, then I agree with you.

[Julian Berman]

I guess to make it explicit, \t is considered way less common to have to type these days to be worth dethroning the mighty arrow?

[Julian Berman]

It's also the case that some users don't use \ as their abbreviation leader key (and therefore don't have this issue to begin with I suppose) -- again without saying I disagree, is it undesirable to first check whether \ is the leader key and then to decide whether to take over n? (In neovim I think this should be feasible.)

[Marc Huisinga]

Julian Berman said:

It's also the case that some users don't use \ as their abbreviation leader key (and therefore don't have this issue to begin with I suppose) -- again without saying I disagree, is it undesirable to first check whether \ is the leader key and then to decide whether to take over n? (In neovim I think this should be feasible.)

If you want to set a different leader key, you should be able to use the 'Custom Translations' setting to override the abbreviations to your liking.

[Marc Huisinga]

Julian Berman said:

I guess to make it explicit, \t is considered way less common to have to type these days to be worth dethroning the mighty arrow?

I personally don't find it annoying very often, so I definitely wouldn't mind if \t keeps mapping to the triangle.

[Arthur Paulino]

I've been very happy with this adjustment
Arthur Paulino said:

Patrick Massot said:

Note that you can also use another input leader (other than \).

IIRC I saw in a video that you use ,. I think that's a smart move and I'm going to copy it :eyes:

[František Silváši 🦉]

I'll just leave this here :).
#lean4 > Keep VS Code from replacing escape sequence? @ 💬

[Eric Rodriguez]

It seems to be a UK QWERTY-only quirk, but ¬ is already on the top left for me

[Edward van de Meent]

Julian Berman said:

I guess to make it explicit, \t is considered way less common to have to type these days to be worth dethroning the mighty arrow?

we already can type \r tho?

[Edward van de Meent]

(fitting in with the \l \d \u pattern for arrow directions)

[Julian Berman]

\r is →, \t is ▸ the used-to-be-Eq.substterm-mode-rewrite thing whose name I never remember. (So I should have said "triangle" clearly) but I think the point is it sounds like that is proposed to stay as is, and if you want to type tab, you "continue" to have the issue described in this thread (and/or you override the abbreviation).

[Edward van de Meent]

i wasn't even thinking about tab, i thought you were suggesting to remove the rewrite triangle abbreviation in favor of the function arrow :upside_down:

[Julian Berman]

Ah no, though I use \to, I had forgotten about r honestly so your mnemonic is good to remind me