If I follow
declaring the instances for Z of
abelian seems to automatically create the one for ring. Now if I move the ring declaration after the instances. The instance for
ring does not seem to be created . Is there a command to get the completion as before?
For now you can write :
HB.instance Definition _ := SemiRing.on Z.
(this will attempt to fill everything again).
But ultimately we should trigger completion on structure addition. I am surprised that we did not register the issue so far.
I added it as a new issue: math-comp/hierarchy-builder#197
A related issue appears here where all possible instances are not present because the parameters differ... We should also provide an automated completion of these at some point.
Hopefully this won't bite us too much in the porting activity, but it is good to have it planned in an issue.
Last updated: May 28 2023 at 18:29 UTC