HB makes me import all the modules down hierarchy chain

[anton-trunov]

For instance, if I need to build on top of order, I need to import order and all its dependencies, i.e. eqtype and choice, otherwise, I get an error message like

The conclusion of a builder is a mixin whose parameters depend on other mixins: extract-conclusion-params
 (prod `record` (app [global (indt «POrder.axioms_»), c3, c4]) c5 \
   app [global (indt «choice.HasChoice.axioms_»), c4]) X0^5

[CohenCyril]

Hi @anton-trunov sorry for the very late answer. We are aware of this limitation and thought of printing a better error message. Would that be good enough for you?

[anton-trunov]

Hi @CohenCyril, yes, a better error message would be great!

Is this limitation documented somewhere? If not, it would be great to have that too.