Mathlib-style formatter

Stream: mathlib4

[Vasily Ilin]

Hi.
Is there a tool that implements the mathlib code style https://leanprover-community.github.io/contribute/style.html? Or at least checks if my code adheres to it.

[Ruben Van de Velde]

Sadly no

[Ruben Van de Velde]

There's a few linters, but nothing complete

[Eric Wieser]

Currently the best "tool" is creating a PR and letting the reviewers advise on style

[Eric Wieser]

If you've read #style and looked at some mathlib code as an example, it's likely you're mostly there