Any idea what I'm doing wrong here? (this is a simplified example extracted from topology.v
in MC Analysis)
From HB Require Import structures.
HB.mixin Record IsA (T' : Type) T := { opA : T -> T' }.
HB.structure Definition A (T' : Type) := {T of IsA T' T}.
HB.mixin Record IsB (T : Type) of A T T := { opB : T }.
Fail HB.structure Definition B (T : Type) := {T of A T T & IsB T}.
(*
axioms_ is defined
test_IsA_mixin is defined
test_IsB_mixin is defined
type is defined
sort is defined
class is defined
phant_clone is defined
pack_ is defined
test_B_class__to__test_A_class is defined
test_B__to__test_A is defined
phant_on_ is defined
T is declared
T0 is declared
HB_unnamed_factory_7 is defined
test_B__to__test_IsA is defined
test_B__to__test_IsB is defined
HB_unnamed_mixin_10 is defined
The command has indeed failed with message:
HB: cannot infer some information in structures_eta__canonical__test_B :
type ?e0 :=
{|
sort := eta T0;
class :=
{|
test_IsA_mixin := HB_unnamed_mixin_4 T0 T0;
test_IsB_mixin := HB_unnamed_mixin_10
|}
|}
*)
Thanks for minimizing & reporting this! I have a lead about what might be going on here. I will investigate.
Pierre Roux has marked this topic as resolved.
c.f. https://github.com/math-comp/hierarchy-builder/issues/298
Last updated: May 28 2023 at 18:29 UTC