Skip to content

Commit 234e3f5

Browse files
authored
Update tests/monoid_enriched_cat.v
1 parent 0821793 commit 234e3f5

File tree

1 file changed

+2
-0
lines changed

1 file changed

+2
-0
lines changed

tests/monoid_enriched_cat.v

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -45,6 +45,8 @@ HB.instance Definition _ (T : Monoid_enriched_quiver.type) (A B : T) : isMon (@h
4545

4646
(* each instance of isMon should be tried as an instance of hom_isMon *)
4747

48+
(* Step 3: for each instance of a wrapped mixin on a subject known
49+
to be wrapped, automatically produce an instance of the wrapper mixin too. *)
4850
HB.instance Definition _ := isQuiver.Build Type (fun A B => A -> B).
4951
Fail HB.instance Definition homTypeMon (A B : Quiver.type) := isMon.Build (hom A B) (* ... *).
5052
(* This last command should create a `Monoid_enriched_quiver`, in order to do so it should

0 commit comments

Comments
 (0)