Alignment of by clauses in reasoning syntax

[VojtechStep]

The code style guidelines describe the following formatting for by clauses

  equational-reasoning
    term-1
    ＝ term-2
      by
      equation-1
    ＝ term-3
      by
      equation-2

However it's becoming more frequent to use

  equational-reasoning
    term-1
    ＝ term-2
      by
        equation-1
    ＝ term-3
      by
        equation-2

There are reasons to prefer either, but I think we should converge on one style and follow it. I'm opening a discussion to see if anyone has a strong reason to prefer the second style. I see it looks more consistent with function application, but in this context we treat by as a keyword, and the first style is consistent with how we treat where w.r.t. reducing right drift. Unless a strong reason is presented, I support enforcing the first style in PR reviews going forward (and writing a lint; rejecting files matching ^( +)by\n\1 + looks sound enough).

[fredrik-bakke]

I support your proposal. In addition, there is a question of wheter the outer indentation should be there too, i.e.,

  equational-reasoning
  term-1
  ＝ term-2
    by
    equation-1
  ＝ term-3
    by
    equation-2

I think this can be justified by the same reasons.

[VojtechStep]

I don't have a strong opinion on that. My knee-jerk reaction is that equational-reasoning behaves more like a function call and delimits a block which constructs a single term, but I admit that might be rationalizing my biases, since I'm already used to the indented style

[fredrik-bakke]

Fair enough. I'm happy to implement only your proposal. The slightly weird thing about function calls is that we format them like

  my-fun
    ( ...)
    ( ...)

but

  ( my-fun
    ( ...)
    ( ...))

meaning that inside a nested expression, equational reasoning would be formatted as I suggest either way. But still, being able to parse the nestedness at a glance is an important feature of our formatting principles,... meaning I might have changed my mind on my extraproposal.

[lowasser]

I'll admit this is a case where I find indentation to help my ability to follow what's going on. I'd cheerfully love to find ways to deindent equational-reasoning more aggressively, however.

It feels significantly more natural to me to indent the body of by when taking into account -- as I strongly prefer to do -- that the by ... block can be consolidated to one line, e.g. by equation-1 all together.

[lowasser]

(To be explicit, this is opposition to the proposal.)

[lowasser]

I might alternately be convinced by

 equational-reasoning
    term-1
    ＝ term-2
    by
      equation-1
    ＝ term-3
    by
      equation-2

keeping the alternating steps of the syntax at the same indentation level, and the nontrivial contents also at the same indentation level.