HbDeclareContext

Setting things up so that a type variable T has all the canonical instances we want, e.g. to test a new structure, is not trivial. The HB.declare command helps you do it.

HB.mixin Record AddComoid_of_Type A := {
  zero : A;
  add : A -> A -> A;
  addrA : forall x y z, add x (add y z) = add (add x y) z;
  addrC : forall x y, add x y = add y x;
  add0r : forall x, add zero x = x;
}.
HB.structure Definition AddComoid := { A of AddComoid_of_Type A }.

Notation "0" := zero.
Infix "+" := add.

HB.mixin Record AbelianGrp_of_AddComoid A of AddComoid_of_Type A := {
  opp : A -> A;
  addNr : forall x, opp x + x = 0;
}.
HB.structure Definition AbelianGrp := { A of AbelianGrp_of_AddComoid A & }.

Notation "- x" := (opp x).

Section Test.
HB.declare Context (T : Type) (p : AddComoid_of_Type T) (q : AbelianGrp_of_AddComoid T).

Goal forall x : T, x + -x = 0.
Abort.

End Test.

Note that, in order to typecheck AbelianGrp_of_AddComoid T, T must be an AddComoid.type canonically. HB.declare takes care to interleave the postulation of section variable with the declaration of canonical instances, and as all other HB commands, desugars factories into mixins.

Finally, code such as:

Section Test.
Variable T : AddComoid.type.
...

works fine unless one tries to call HB.instace to enrich T further.