-
Notifications
You must be signed in to change notification settings - Fork 20
HbDeclareContext
Enrico Tassi edited this page Jun 18, 2021
·
4 revisions
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.instance
to enrich T
further.