indenting variables

Stream: general

[Scott Morrison]

A boring style guide question:

[Scott Morrison]

/poll Should multi-line variables statements indent the second and later lines?

[Scott Morrison]

Currently we're somewhat inconsistent in mathlib. I think I'm in favour of Yes, on the basis that it seems analogous to indenting multi-line theorem statements.

[Eric Wieser]

Many of the cases I've seen instead "indent" with the word variables, as

variables {long : Type*}
variables {longer : Type*}

instead of

variables {long : Type*}
  {longer : Type*}

or

variables {long : Type*}
          {longer : Type*}

[Scott Morrison]

One reason to become prescriptive about the style guide on boring points like this is that in the near future the entirety of mathlib is going to be reformated by a computer (when synport magically turns mathlib3 into mathlib4). If we don't actually decide what we want, we'll get something arbitrarily chosen instead. (While in Lean4 it will be easier to write formatting linters, we may as well get these things write the first time.)