search

leanprover / lean3

Lean Theorem Prover
http://leanprover.github.io/
Apache License 2.0
2.15k stars 217 forks source link

leanfmt: Lean code formatter #1970

Open alok opened 6 years ago

alok commented 6 years ago

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

Kha commented 6 years ago

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 commented 6 years ago

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

--- Alok

On Wed, Aug 29, 2018 at 5:01 PM Sebastian Ullrich notifications@github.com 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 https://github.com/leanprover/lean/issues/1970#issuecomment-417146412, or mute the thread https://github.com/notifications/unsubscribe-auth/AH8KTJkBg6SPiZOdmL8lkF62BdlvBwTbks5uVys_gaJpZM4WSjYj .