leanprover
Abbreviations / Unicode-Input Improvement Discussion
I have some thoughts about unicode-input improvements that I would like to discuss. Maybe they can improve working with non-ascii characters.
-
99% of the times when I type
a1,b1,h2, ..., I meana₁,b₁,h₂. Maybe such replacements could happen automatically, whena1,b1, ... does not appear anywhere in the current document, buta₁, ... does? Should be easy to implement with an index of all words (i.e.\S+) in the current document. It would be nice if declaration vs usage could be distinguished, but I guess this will only be possible with Lean 4. -
I think it might be sensible to replace
<->and->automatically with their unicode equivalent. (See next point) -
Many abbreviations are not prefix-free, i.e. there are abbreviations
aandabsuch thatais a prefix forab. This means that when\ahas been typed, it could be extended to\ab. Abbreviations that don't have such an extension can be replaced immediately when the last character is inserted. Maybe this can also be implemented for abbreviations that actually have an extension (like\<->)? The replacement would be temporarily and needs to be reverted when another character is added. Maybe some ~300ms timeout could be used to defer replacement of extendable abbreviations.
What do you think?
First, thanks for thinking about the extension! There are certainly lots of improvements that could be made; I think many of the UX decisions up to now have been governed more by ease of implementation / hacks rather than by any principled decisions.
In my opinion, (1) and (2) sound a bit too much like magic to me to have them always on by default, but they seem like reasonable optional settings. (3) sounds interesting; I like the first part of (3) more than the second, but I'd have to test it out to be sure.
A large community of Lean users hangs out at the Lean prover community Zulip, so you may get more comments if you post there.
I already implemented the first part of (3) in #240! You can try it out there.