Lean unicode

Stream: general

[King Arthur]

is it possible to use the lean unicode backslash shortcuts outside of .lean files?

[Johan Commelin]

See https://github.com/gebner/m17n-lean

[King Arthur]

might be a bit overkill actually haha. is there a way to just enable it for other file extensions in vscode? (or specific files even)

[Horațiu Cheval]

I use this extension: https://marketplace.visualstudio.com/items?itemName=yellpika.latex-input to write unicode everywhere in vscode

[Eric Wieser]

is there a way to just enable it for other file extensions in vscode?

Yes, this is configurable in the vscode settings

[King Arthur]

I found the setting for enabling lean unicode input in other file types, but I tried adding "txt" or ".txt" or "text document" etc. and it wouldn't work for some reason

[King Arthur]

I use this extension: https://marketplace.visualstudio.com/items?itemName=yellpika.latex-input to write unicode everywhere in vscode

I tried this one and it's alright I think. I do prefer the one that lean has for a few reasons however