Skip to content

Commit b7f3789

Browse files
authored
Update tests/monoid_enriched_cat.v
1 parent 92e1f68 commit b7f3789

File tree

1 file changed

+3
-0
lines changed

1 file changed

+3
-0
lines changed

tests/monoid_enriched_cat.v

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -31,6 +31,9 @@ Fail HB.structure
3131
- the wrapped mixin (`isMon`)
3232
- the wrapper mixin (`hom_isMon`)
3333
- the new subject (`hom`)
34+
This attribute will add an entry in the `wrapper-mixin` database.
35+
As an addition substep, we should check that the wrapper has
36+
exactly one field, which is the wrapped mixin.
3437
*)
3538
#[wrapper]
3639
HB.mixin Record hom_isMon T of Quiver T :=

0 commit comments

Comments
 (0)