search

math-comp / hierarchy-builder

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

Missing coercions to factories #207

Open CohenCyril opened 3 years ago

CohenCyril commented 3 years ago

If we have a structure S := {T of m T} composed of one mixin m, there is a coercion from S to m (which is currently available and reliable upon).

Now if mixin is turned into a factory which is equivalent to two new mixins m1 and m2 (we have builders m -> m1 and m -> m2), then there are now two coercions S -> m1 and S -> m2, but no more S -> m, we must add it. We should add a new command for that, e.g. HB.yields f where f has type S -> m.

Note that this actually means m <-> m1 * m2, and that would not be true for all factories, but it must be true for mixins that get turned into factories, because the point is that the structure contents must stay the same (up to iso).

In further versions we might actually want to verify this is an iso, but this is longer term.

CohenCyril commented 10 months ago

I suggest implementing a command HB.cobuilder that takes a factory as argument, which automatically assumes the maximal class entailed by this factory and invites the user to build the factory.