Stream: Hierarchy Builder devs & users

Topic: Generated Instances


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Cyril Cohen (Apr 01 2021 at 16:27):

I added it as a new issue: math-comp/hierarchy-builder#197

view this post on Zulip 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.

view this post on Zulip 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: Jan 29 2023 at 15:02 UTC