hierarchy-builder icon indicating copy to clipboard operation
hierarchy-builder copied to clipboard

Published 20 hours ago • verified publisher icon math-comp

Support for universe polymorphism

Open jonsterling opened this issue 3 years ago • 3 comments

It would be game-changing to support universe polymorphism. Right now I have a class of large categories, and this is enough for me at the moment, but I would be able to do things so much nicer if I could also speak of small categories without duplicating everything. I realize this is probably quite complex engineering-wise.

jonsterling avatar Dec 13 '21 19:12 jonsterling

in progress... @ecranceMERCE is helping, we will get there. tracker: https://github.com/LPCIC/coq-elpi/pull/315

gares avatar Dec 13 '21 20:12 gares

Any news on this front?

HB.mixin breaks syntactically if I "Set Universe Polymorphism", and it says "Attribute universes.polymorphic is not supported" if I start the declaration with "#[universes(polymorphic=yes)]".

damien-pous avatar Jul 29 '23 18:07 damien-pous

Well, we started but it far from being done. I suggest you Unset universe checking in the meanwhile.

gares avatar Jul 29 '23 21:07 gares