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?

Do you mean the extension should support inserting mathematical Unicode characters? I guess 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.