Zulip Chat Archive

Stream: mathlib4

Topic: Line-wrapping of infix operators


Eric Wieser (Oct 13 2023 at 11:48):

How should the following be formatted?

theorem forget₂_map_associator_hom (X Y Z : AlgebraCat.{u} R) :
    (forget₂ (AlgebraCat R) (ModuleCat R)).map (associator X Y Z).hom
      = (α_
        (forget₂ _ (ModuleCat R) |>.obj X)
        (forget₂ _ (ModuleCat R) |>.obj Y)
        (forget₂ _ (ModuleCat R) |>.obj Z)).hom := by
  rfl

#style suggests that = (as an "infix operator") should be on the end of the previous line rather than the start of the next; but I'd argue this makes it harder to separate the LHS and RHS, especially if both contain line wrapping.


Last updated: Dec 20 2023 at 11:08 UTC