Stream: Constructive reals & analysis

Topic: Rationals

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Bas Spitters (Aug 04 2020 at 20:21):

Yes, moving them to the platform is a first goal now.

Last updated: Apr 21 2024 at 01:02 UTC