test

Author: gares

_CoqProject.test-suite

@@ -95,7 +95,10 @@ tests/unit/close_hole_term.v
 tests/unit/struct.v
 tests/factory_when_notation.v
 
+tests/test_primproj_ty.v
+
 -R tests HB.tests
 -R examples HB.examples
 
+
 -Q . HB

tests/test_primproj_ty.v

@@ -0,0 +1,21 @@
+From Coq Require Import ssreflect ssrfun.
+From HB Require Import structures.
+
+#[primitive]
+HB.mixin Record AddMonoid_of_TYPE S := {
+  zero : S;
+  add : S -> S -> S;
+  addrA : associative add;
+  add0r : left_id zero add;
+  addr0 : right_id zero add;
+}.
+
+HB.structure Definition AddMonoid := { A of AddMonoid_of_TYPE A }.
+
+Set Printing All.
+
+Goal let x := @addrA in True.
+match goal with
+| |- let x : forall s : AddMonoid.type, @associative (AddMonoid.sort s) (@add s) := @addrA in True => idtac "OK"
+end.
+Abort.