Does the extension need to manage typing Unicode characters?

[ornamentist]

Lean 4 syntax allows a range of mathematical Unicode characters to be used. Does the extension need to allow inserting these or should that be handled by a separate Zed extension or LSP provider?

[owlx56]

Does the extension need to allow inserting these or should that be handled by a separate Zed extension or LSP provider?

It can be supported by lean 4 snippets. The snippets can exist as a separate extension or be integrated into this extension.

For more information, please check docs.

[ornamentist]

Thanks -- they're good options.

[owlx56]

Now Zed Lean 4 supports Abbreviation (unicode character) insertion by snippets.

[castedo]

Another approach is to use your operating system to let you type math unicode. That is what I do. Here are instructions for UNIX-like operating systems:

https://castedo.gitlab.io/vim9-lean/math-input/

I imagine on MacOS and Windows there is something similar.