Unicode macros for Lean language

[bonsairobo]

It would significantly improve the experience of editing Lean code if Helix had support for unicode macros, like VSCode has, as described here:

The editor shares a number of features with Visual Studio Code; for example, you can type unicode characters with a backslash, so \and yields the unicode symbol for conjunction, and \a, \b, and \g yield the unicode α, β, and γ respectively.

The behavior present in the "lean4" vscode plugin is that you can just type "\a" and then <space> and the "\a" will be replaced with "α".

[pascalkuthe]

This could be either implemented using abbreviations (#1471) or unicode diagraph support (#1438). Both of which should be implemented using a future snippet system IMO.

This feature request is too specific, we don't adllow any language specific code in core.