search

math-comp / hierarchy-builder

High level commands to declare a hierarchy based on packed classes
MIT License
96 stars 21 forks source link

Cannot declare an instance on a function type #440

Closed pi8027 closed 1 month ago

pi8027 commented 1 month ago

@Tragicus reported that HB.instance does not let us declare an instance on a function type. Since canonical structures allow such an instance declaration (since Coq 8.14, coq/coq#14386), I imagine it is just not implemented in HB.

proux01 commented 1 month ago

Do we have a concrete minimal example, I would expect HB now to support all coercion classes (Sort, Function and gref)

Tragicus commented 1 month ago

I think the issue we saw is that A -> B is not a choiceType (and not even an eqType), so when I try to give it any structure that requires it, nothing happens. I just tested with a dummy pointedType structure and it works.

proux01 commented 1 month ago

So, looks like you're one more victim of https://github.com/math-comp/hierarchy-builder/issues/348 Should we close this then?

Tragicus commented 1 month ago

Yes... I think so.