Laurent Théry (Apr 01 2021 at 16:03): Laurent Théry (Apr 01 2021 at 16:03):If I follow https://github.com/math-comp/hierarchy-builder/blob/master/examples/Coq2020_material/CoqWS_demo.v
declaring the instances for Z of semiring and 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?
Cyril Cohen (Apr 01 2021 at 16:24):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.
Cyril Cohen (Apr 01 2021 at 16:27):I added it as a new issue: math-comp/hierarchy-builder#197
Cyril Cohen (Apr 01 2021 at 16:29):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.
Enrico Tassi (Apr 01 2021 at 19:51):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