style guide

Stream: general

[Scott Morrison]

I'm making some edits to style.md on the community website.

I wanted to ask about one section:

Use two spaces to indent. You can use an extra indent when a long line
forces a break to suggest the break is artificial rather than
structural, as in the statement of theorem:

```lean
open nat
theorem two_step_induction_on {P : nat → Prop} (a : nat) (H1 : P 0) (H2 : P (succ 0))
    (H3 : ∀ (n : nat) (IH1 : P n) (IH2 : P (succ n)), P (succ (succ n))) : P a :=
sorry
```

If you want to indent to make parameters line up, that is o.k. too:
```lean
open nat
theorem two_step_induction_on {P : nat → Prop} (a : nat) (H1 : P 0) (H2 : P (succ 0))
                              (H3 : ∀ (n : nat) (IH1 : P n) (IH2 : P (succ n)), P (succ (succ n))) :
  P a :=
sorry
```

[Scott Morrison]

It seems we now follow neither of these pieces of advice. (i.e. people just use a two space indent if there are too many hypotheses to fit on a line, and we actively discourage doing long indents in this situation).

[Scott Morrison]

If there's general agreement on this point, I'll simply remove these two paras.

[Johan Commelin]

We do follow the advice when formatting calc blocks

[Johan Commelin]

So maybe we should rather change it a bit... or are calc blocks already dealt with separately?

[Scott Morrison]

Yes, there's already a separate section on calc blocks, indicating that you should try to line things up (possibly excepting the first line).

[Johan Commelin]

In that case, I don't mind if you delete these 2 paras

[Scott Morrison]

Done.