readability

Stream: general

[Kind Bubble]

I'm new to Lean and I've made some mistakes involving readability of code.

Right now I'm collecting some readability conventions and I'd appreciate it if people chimed in about precedents that they appreciate. Here are some I've found:

1) Keep each line of code to 100 characters or less.
2) Mind natural spaces even if it compiles.
3) Label lemmas, theorems, and definitions accordingly.

What are some others?

[Junyan Xu]

Have you seen https://leanprover-community.github.io/contribute/style.html ?
There are linters that basically 1) and 3), but for 2) we are waiting for Lean 4 which makes auto-formatting easy.