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?
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: Oct 13 2024 at 01:02 UTC