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