hierarchy-builder
hierarchy-builder copied to clipboard
math-comp
High level commands to declare a hierarchy based on packed classes
As mentioned in the corresponding Zulip thread, the following code fails with the error "term->gref: input has no global reference", which is not very clear. Here, `id` should be replaced...
Example ```coq From HB Require Import structures. From Coq Require Import Relations Morphisms. HB.mixin Record hasEquiv A := { equiv : relation A }. HB.structure Definition Equiv := { A...
For now, when calling HB.instance on a term that is not of type mixin or doesn't typecheck or has unsolvable holes, the error message is not readble.
- do a saturation of potential joins. - check for multiple instances for a same type, coming from multiple modules (refer to [orphan instances in Haskell](https://wiki.haskell.org/Orphan_instance)) cc @RobbertKrebbers Bonus questions:...
It might be nice for the users to be informed when using `HB.howto` (for example, by a message in the output) that they can increase the "depth search" to potentially...
`HB.about` should indicate which argument is the key of the structure / factory / factory `.Build` and explicit the fact that it is a bad practice to leave it implicit.
These two commands should give pointers to one another e.g. - `HB.about C`, where `C` is a class, should say ``` C is a class, the associated type is `ctype`...
``` HB.howto GRing.Ring.type GRing.SubRing.type. HB.about GRing.isSubSemiRing. About GRing.valM_subproof. ``` Also hide the _subproof ugly suffix