Bas Spitters (Aug 04 2020 at 20:11): Bas Spitters (Aug 04 2020 at 20:11):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.
Karl Palmskog (Aug 04 2020 at 20:14):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.
Bas Spitters (Aug 04 2020 at 20:21):Yes, moving them to the platform is a first goal now.
Last updated: Oct 13 2024 at 01:02 UTC