Skip to content

Commit d2bc00f

Browse files
authored
Update tests/monoid_enriched_cat.v
1 parent 17d6561 commit d2bc00f

File tree

1 file changed

+6
-1
lines changed

1 file changed

+6
-1
lines changed

tests/monoid_enriched_cat.v

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -34,4 +34,9 @@ HB.instance Definition _ (T : Monoid_enriched_quiver.type) (A B : T) : isMon (@h
3434

3535
(* each instance of isMon should be tried as an instance of hom_isMon *)
3636

37-
37+
HB.instance Definition _ := isQuiver.Build Type (fun A B => A -> B).
38+
Fail HB.instance Definition homTypeMon (A B : Quiver.type) := isMon.Build (hom A B) (* ... *).
39+
(* This last command should create a `Monoid_enriched_quiver`, in order to do so it should
40+
automatically instanciate the wrapper `hom_isMon`:
41+
HB.instance Definition _ := hom_isMon.Build Type homTypeMon.
42+
*)

0 commit comments

Comments
 (0)