Zulip Chat Archive

Stream: mathlib4

Topic: aligning Bicategory fields

Kevin Buzzard (Feb 16 2023 at 06:16):

@Matthew Ballard you PRed bicategories and I'm porting another file in the bicategory repo because I was tricked into doing so by Adam. But the autoporter is still translating the field whiskerLeft_comp to whisker_left_comp. Do all the fields need to be aligned manually?

Matthew Ballard (Feb 16 2023 at 13:23):

Sorry. I’ll fix that.

Matthew Ballard (Feb 16 2023 at 18:51):

Fixed now in that PR. Working on fixing the missing Bicategory.Basic #align’s and other missing ones in a separate PR.

Last updated: Dec 20 2023 at 11:08 UTC