Stream: Hierarchy Builder devs & users

Topic: Mixin towards non-HB mixin records


view this post on Zulip abab9579 (Sep 05 2022 at 06:21):

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.

view this post on Zulip Pierre Roux (Sep 05 2022 at 07:13):

Building HB hierarchies on top of non HB ones is not impossible but is very hackish. I certainly wouldn't recommend it.

view this post on Zulip abab9579 (Sep 05 2022 at 07:17):

I see, so would I better align with the non-HB hierarchy in this case?

view this post on Zulip Enrico Tassi (Sep 05 2022 at 08:07):

What do you mean by "ssreflect"? The mathcomp library?

view this post on Zulip abab9579 (Sep 05 2022 at 08:13):

My bad, I thought ssreflect was the name of the library. I meant libraries of https://math-comp.github.io/ .

view this post on Zulip Enrico Tassi (Sep 05 2022 at 08:15):

Then we are porting them to HB, see https://github.com/math-comp/math-comp/pull/733

view this post on Zulip Enrico Tassi (Sep 05 2022 at 08:16):

and along with it MC analysis & co

view this post on Zulip abab9579 (Sep 05 2022 at 09:38):

Sounds great! Looking forward to the update.


Last updated: Jan 29 2023 at 15:02 UTC