Newline in #align

Stream: mathlib4

[Yury G. Kudryashov]

@Eric Wieser Does your automation about #align (if any) allows newlines instead of spaces like in

#align add_subgroup.zsmul_mem_zmultiples_iff_exists_sub_div
    AddSubgroup.zsmul_mem_zmultiples_iff_exists_sub_div

#align
  finset.order_emb_of_fin_eq_order_emb_of_fin_iff Finset.orderEmbOfFin_eq_orderEmbOfFin_iff

or you want me to search&replace all these newlines?

[Eric Wieser]

I have no automation for that, but I think there is a script elsewhere that does

[Johan Commelin]

I think that all bots are capable of handling newlines, but I still think we should encourage 1-liners so that the occasional grep also just works.

[Johan Commelin]

Maybe we should even lint against ^#align that isn't followed by at least two words.

[Yury G. Kudryashov]

^#align ?[^ ]* ?$ with some \s?

[Johan Commelin]

Sometimes we have comments after #align statements. And I think we should allow those