Zulip Chat Archive

Stream: general

Topic: readability

Kind Bubble (Jan 22 2023 at 06:32):

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 (Jan 22 2023 at 06:45):

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.

Last updated: Aug 03 2023 at 10:10 UTC