Open jonsterling opened 3 years ago
There is a Zulip stream you can use for questions.
I would consider this a bug, anyway. You can work around it by using
HB.mixin Record IsCategory 𝒞 of IsPrecategory 𝒞 & isGraph 𝒞 := {}.
or
HB.mixin Record IsCategory 𝒞 of Precategory 𝒞 := {}.
which mean the same.
Let's see what @CohenCyril things about this error
We did not close mixins deps transitively, we should do it or warn (or add an attribute). Thanks for reporting
FTR with #252 the error is even worse (elpi fails), we should fix both problem before the next release
Hi all, thanks very much for looking into this! I have some other questions but I don't want to spam your tickets until I know if they are bugs. Which zulip stream do you prefer I use? I am logged into the Coq zulip.
Hi @jonsterling here is the appropriate stream Hierarchy-Builder stream
I am trying to define categories using HB and ran into a little issue that I wasn't sure how to deal with; am sorry if opening a ticket is not the right place for me to ask for help, please let me know if there is another place where I should ask. Here is what I tried to do:
The last clause throws the following error: