Hello, just trying out HB for usage with ssreflect. Is it impossible to declare mixins towards non-HB mixin records?
When I tried, it just listed the parent mixin as a parameter - it did not recognize the mixin.
Building HB hierarchies on top of non HB ones is not impossible but is very hackish. I certainly wouldn't recommend it.
I see, so would I better align with the non-HB hierarchy in this case?
What do you mean by "ssreflect"? The mathcomp library?
My bad, I thought ssreflect was the name of the library. I meant libraries of https://math-comp.github.io/ .
Then we are porting them to HB, see https://github.com/math-comp/math-comp/pull/733
and along with it MC analysis & co
Sounds great! Looking forward to the update.
abab9579 has marked this topic as resolved.
Last updated: Dec 06 2023 at 14:01 UTC