Stream: Hierarchy Builder devs & users

Topic: ✔ Setting a parameter equal to the carrier

view this post on Zulip Pierre Roux (Jul 22 2022 at 14:24):

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

view this post on Zulip Cyril Cohen (Jul 22 2022 at 15:58):

Thanks for minimizing & reporting this! I have a lead about what might be going on here. I will investigate.

view this post on Zulip Notification Bot (Jul 25 2022 at 09:15):

Pierre Roux has marked this topic as resolved.

view this post on Zulip Pierre Roux (Jul 25 2022 at 09:16):


Last updated: Apr 21 2024 at 01:02 UTC