Lean4 file icon

Stream: new members

[Asei Inoue]

When I open a directory containing .lean files in an editor such as VSCode, I find it sad that there are no icons.

Do you plan to provide icons for .lean files?

[Sky Wilshaw]

I don't know about official support, but you can get this behaviour with an icon file of your own using an extension like <https://marketplace.visualstudio.com/items?itemName=PKief.material-icon-theme>.

[Asei Inoue]

I want an official icon.