leanfmt: Lean code formatter

[alok]

I'd like a way to autoformat lean code, if it exists.

[Kha]

There is no such tool yet. However, the next version of Lean, Lean 4, will provide users with access to a concrete syntax tree representation of Lean code, which should make it much more feasible to write such a tool.

[alok]

Cool. Any (rough) ETA for Lean 4's release?

…

--- Alok

On Wed, Aug 29, 2018 at 5:01 PM Sebastian Ullrich ***@***.***> wrote: There is no such tool yet. However, the next version of Lean, Lean 4, will provide users with access to a concrete syntax tree representation of Lean code, which should make it much more feasible to write such a tool. — You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub <#1970 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AH8KTJkBg6SPiZOdmL8lkF62BdlvBwTbks5uVys_gaJpZM4WSjYj> .