Skip to content

Commit 0821793

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

File tree

1 file changed

+8
-0
lines changed

1 file changed

+8
-0
lines changed

tests/monoid_enriched_cat.v

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -22,6 +22,14 @@ Fail HB.structure
2222
(forall A B : Obj, isMon (@hom (Quiver.clone Obj _) A B)) }.
2323

2424

25+
(* Step 0: define a wrapper predicate in coq-elpi *)
26+
(* Step 1: add a wrapper attribute to declare wrappers,
27+
they should index:
28+
- the wrapped mixin (`isMon`)
29+
- the wrapper mixin (`hom_isMon`)
30+
- the new subject (`hom`)
31+
*)
32+
#[wrapper]
2533
HB.mixin Record hom_isMon T of Quiver T :=
2634
{ private : forall A B, isMon (@hom T A B) }.
2735

0 commit comments

Comments
 (0)