From discussion with @Vincent Semeria:
The stdlib rationals were once ported from corn by Pierre Letouzey. There are more lemmas and tactics for the rationals in corn/math-classes.
To allow more people to profit from them they could be moved to the stdlib, however, this would make corn depend on 8.13.
This seems like the kind of proof engineering issue that @Karl Palmskog likes to think about.
ah, this seems more like a practical everyday proof engineering issue than a proof engineering research issue. Personally, right now, I think the best thing would be if we could get both CoRN and MathClasses into the Coq platform, and take it from there. For example, one may be able to "preserve" platform functionality by simply swapping it from one library to another.
Yes, moving them to the platform is a first goal now.
Last updated: Feb 06 2023 at 06:29 UTC