Stream: Hierarchy Builder devs & users

Topic: Ignoring canonical projection


view this post on Zulip Karl Palmskog (Oct 14 2023 at 10:01):

When porting a project to MC2, I got this warning a couple of times:

Warning: Ignoring canonical projection to eq_op by hasDecEq.eq_op in
HB_unnamed_factory_1: redundant with HB_unnamed_factory_12
[redundant-canonical-projection,records,default]

Can this safely be ignored and/or is there any way to fix it?

view this post on Zulip Pierre Roux (Oct 14 2023 at 10:08):

At least currently in mathcomp, it seems we are ignoring it

-arg -w -arg -redundant-canonical-projection

(which feels bad but I don't have any other solution)


Last updated: Apr 21 2024 at 01:02 UTC