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.


Last updated: Jan 29 2023 at 15:02 UTC