more

_CoqProject.test-suite

@@ -81,6 +81,7 @@ tests/fun_instance.v
 tests/issue284.v
 tests/issue287.v
 tests/monoid_law_structure.v
+tests/monoid_law_structure_clone.v
 
 -R tests HB.tests
 -R examples HB.examples

tests/monoid_law_structure.v

@@ -15,6 +15,4 @@ HB.mixin Record isPreMonoid T := {
 HB.structure Definition PreMonoid := { T of isPreMonoid T }.
 
 HB.structure Definition Monoid :=
- { T of isPreMonoid T &
- isMonLaw T zero add }.
- (* isMonLaw T (@zero (PreMonoid.clone T _)) (@add (PreMonoid.clone T _))*)
+ { T of isPreMonoid T & isMonLaw T zero add }.

tests/monoid_law_structure_clone.v

@@ -0,0 +1,19 @@
+From HB Require Import structures.
+
+HB.mixin Record isMonLaw T (e : T) (op : T -> T -> T) := {
+ opmA : forall a b c, op (op a b) c = op a (op b c);
+ op1m : forall x, op e x = x;
+ opm1 : forall x, op x e = x;
+}.
+
+HB.structure Definition MonLaw T e := { op of isMonLaw T e op }.
+
+HB.mixin Record isPreMonoid T := {
+ zero : T;
+ add : T -> T -> T;
+}.
+HB.structure Definition PreMonoid := { T of isPreMonoid T }.
+
+HB.structure Definition Monoid :=
+ { T of isPreMonoid T &
+ isMonLaw T (@zero (PreMonoid.clone T _)) (@add (PreMonoid.clone T _)) }.