Stream: Hierarchy Builder devs & users

Topic: ✔ More Tool Support


view this post on Zulip Notification Bot (Nov 03 2023 at 09:30):

Laurent Théry has marked this topic as resolved.

view this post on Zulip Cyril Cohen (Nov 03 2023 at 16:26):

Pierre Roux said:

Do we really want to silence the warning? Shouldn't we rather, when adding a canonical instance, check if it already exist (and maybe also check that the already existing one is indeed the expected one)?

These warnings are about projections that are not used for canonical inference. They keep getting the same keys because the proofs or ops may be the same (or have the same head symbol), but not the main key (S.sort) which must be different each time, and for these: yes there should be a check in HB that occurs before Coq discovers a duplicate key. The latter problem should indeed have the solution you described, whereas the former (which AFAIK is the one Laurent encounters) should be solved by informing Coq which projections are not keyed.


Last updated: Oct 13 2024 at 01:02 UTC