Closed FR-vdash-bot closed 6 months ago
Todo: PtReduce typeclass to help infer PtNe instance (we cannot use tactics such as dsimp when inferring a instance) NonCollinear typeclass try to replace XxxND (and some other variants) with Xxx.IsND typeclasses
PtReduce
PtNe
dsimp
NonCollinear
XxxND
Xxx.IsND
Todo:
PtReducetypeclass to help inferPtNeinstance (we cannot use tactics such asdsimpwhen inferring a instance)NonCollineartypeclass try to replaceXxxND(and some other variants) withXxx.IsNDtypeclasses