I notice that there is currently no formalisation of the inclusion order on {set T}. Is there one in the pipeline ? Would you be interrested to have one contributed ? I need an isomorphic one and I realised that I could define mine by isomorphism.
Please do contribute it to order.v
.
Also, I just noticed that the documentation of Iso mixup IsoLatticeMixin
and IsoDistrLatticeMixin
and that there is no IsoBLattice
, IsoTBLattice
and friend... What do you think about a unique IsoLatticeMixin
which coerce to the various lattices mixins depending on the structures on the isomorphic lattice. Is this implementable ?
I tried and I'm stuck with uniform inheritance condition problem... I'll try again later...
Maybe should we wait for HB to do that kind of changes, in order to avoid doing the job twice?
I just submitted a PR defining subset order on {set T}
. As suggested by @Pierre Roux I'm keeping the Mixin stuff for after HB.
Last updated: Mar 28 2024 at 23:01 UTC