style: indenting termination_by and decreasing_by

Stream: general

[Johan Commelin]

Should termination_by and decreasing_by be indented or not?
Mathlib seems to have both styles occurring quite a bit.

[Damiano Testa]

I don't have a strong opinion, though maybe have a slight preference for no indentation.

[Johan Commelin]

Same here

[Julian Berman]

I followed https://github.com/leanprover/vscode-lean4/pull/329/files in lean.nvim which had proposed indenting for them (but of course am happy to change). I think I didn't even find any examples of multi-line termination_by, but I found lots of examples for decreasing_by and at least in core I think they were all indented.

[Joachim Breitner]

Purely personal preference, but I find I don’t indent them. They are not part of the typically indented body of the function. Likewise, I also don’t indent where.

The lean core repo also has both styles:

~/build/lean/lean4 $ git grep ^\ \ termination_by|wc -l
130
~/build/lean/lean4 $ git grep ^termination_by|wc -l
433
~/build/lean/lean4 $ git grep ^\ \ \ \ termination_by|wc -l
34

(Although that could be misleading, as the “don’t indent” rule would indent it if is part of a where or letrec defined function).