style guidelines

Stream: lean4

[Bhakti Shah]

the style guidelines here are i think very different from Lean 4 code i've looked at (presumably because lean 4 style is very different from lean 3) -- would someone mind clarifying the following conventions for lean 4 style? some of them might seem silly but i just wanted to be thorough so any amount would be helpful :)
- type names (case)
- type constructor names (case)
- function names (case)
- theorem names (case)

• indentation
• nested matches / do blocks (indentation / parenthesizing)
  thank you!
  (edit: some of these are answered by this and a different thread)

[Jireh Loreaux]

Indentation:

1. continued statements of declarations are indented four spaces
2. the body of a declaration is (initially) indented two spaces
3. If the proof is a tactic proof, the by should appear on the line prior to the body.

For example:

lemma my_result ...... :
    ....... := by
  my_tactic

[Jireh Loreaux]

As for do blocks, I think the goal is to handle everything with more indentation, and eschew parenthesizing, but I'm not positive about this.

[Jireh Loreaux]

There's also this

[Bhakti Shah]

thanks! that helps a ton