test

Author: gares

_CoqProject.test-suite

@@ -68,7 +68,7 @@ tests/lock.v
 tests/interleave_context.v
 tests/not_same_key.v
 #tests/factory_sort.v
-tests/factory_sort_tac.v
+tests/hb_pack.v
 tests/declare.v
 tests/short.v
 tests/primitive_records.v

tests/factory_sort_tac.v renamed to tests/hb_pack.v

@@ -111,4 +111,15 @@ pose X := Foo.pack T (HasFoo.Build A P T H).
 Check X : Foo.type A P.
 Abort.
 
-End test2.
+End test2.
+
+HB.mixin Record isID T (F : T -> T) := { p : forall x : T, F x = x }.
+HB.structure Definition Fun T := { F of isID T F }.
+
+Goal forall f : nat -> nat, forall p : (forall x, f x = x ), True.
+intros f p.
+pose F := isID.Build nat f p.
+pose T : Fun nat := HB.pack nat f F.
+Check T : Fun.type nat.
+Abort.
+