Hi, I am doing my night classes. Where can I find the flags that exists like
mathcomp and what they are doing?
The best "doc" is here: https://github.com/math-comp/hierarchy-builder/blob/master/structures.v#L331
@Cyril Cohen I don't have the button to make a thread out of these 2 messages, please use your suporpowers
[#mathcomp] the notations
[myStructureType of ...] is not generated?
No, our dear coq-elpi maintainer did not bind string notations yet...
Last updated: Jan 29 2023 at 15:02 UTC