Stream: Hierarchy Builder devs & users

Topic: HB command attributes


view this post on Zulip Laurent Théry (Apr 01 2021 at 14:32):

Hi, I am doing my night classes. Where can I find the flags that exists like verbose and mathcomp and what they are doing?

view this post on Zulip Enrico Tassi (Apr 01 2021 at 14:34):

The best "doc" is here: https://github.com/math-comp/hierarchy-builder/blob/master/structures.v#L331

view this post on Zulip Enrico Tassi (Apr 01 2021 at 14:34):

@Cyril Cohen I don't have the button to make a thread out of these 2 messages, please use your suporpowers

view this post on Zulip Laurent Théry (Apr 01 2021 at 14:43):

So in [#mathcomp] the notations [myStructureType of ...] is not generated?

view this post on Zulip Cyril Cohen (Apr 01 2021 at 14:45):

No, our dear coq-elpi maintainer did not bind string notations yet...


Last updated: Jan 29 2023 at 15:02 UTC