test for step 0 of CoREACT #357

gares · 2023-06-02T13:16:03Z

No description provided.

tests/monoid_enriched_cat.v

CohenCyril · 2023-06-19T14:16:40Z

tests/monoid_enriched_cat.v

+(* This last command should create a `Monoid_enriched_quiver`, in order to do so it should
+  automatically instanciate the wrapper `hom_isMon`:
+  HB.instance Definition _ := hom_isMon.Build Type homTypeMon.
+   *)


Suggested change

*)

*)

(* Step 4: automatically produce the wrapper mixin *)

tests/monoid_enriched_cat.v

CohenCyril · 2023-06-19T14:29:17Z

tests/monoid_enriched_cat.v

+(* 5 lines of documentation + 1 line of elpi code in structure.v
+  `pred wrapper-mixin o:mixinname, o:gref, o:mixinname`
+*)
+(* Step 1: add a wrapper attribute to declare wrappers,


Here is the code for attribute declaraion

hierarchy-builder/HB/common/utils.elpi

Lines 26 to 40 in 3b54647

coq.parse-attributes A [

att "verbose" bool,

att "mathcomp" bool,

att "mathcomp.axiom" string,

att "short.type" string,

att "short.pack" string,

att "infer" attmap,

att "key" string,

att "arg_sort" bool,

att "log" bool,

att "log.raw" bool,

att "compress_coercions" bool,

att "export" bool,

att "skip" string,

att "local" bool,

You can then use the get-option predicate to find the value of an attribute

gares added 4 commits June 2, 2023 15:15

test for step 0 of CoREACT

6f1dee6

update

1ceb6ea

more

f6c1970

more

17d6561

CohenCyril reviewed Jun 15, 2023

View reviewed changes

tests/monoid_enriched_cat.v Outdated Show resolved Hide resolved

Update tests/monoid_enriched_cat.v

d2bc00f