Hi,

I need to turn strings with float numbers, e.g. 1.02 or 1.01e-1 into decimal (from Coq.Init.Decimal) or floats. I understand there might be rounding issues with the latter, and this is OK for the demo I planned.

What is not clear is what the most direct approach is and whether or not some existing code exists.

Parsing a string from a decimal (e.g. 1.02) should be straightforward using int_of_string and the like.

I am confused at the last leg: going from decimal to a float.

Any hint to share? Thanks!

floating points and strings were recently discussed here, maybe helpful?

Thanks. That's for string_of_float though. I am curious about what could be float_of_string. I'll dig some of the links there.

@Jerome Hugues the file in https://github.com/coq/coq/issues/14782#issuecomment-906480643 should contain a solution.

Note that to do pretty much anything with floats, it is advised to use the dedicated library Flocq. The Floats module in the stdlib is only intended to provide access to primitive floats in the kernel, which is only useful for fast floating-point computations inside Coq (to implement reflexive tactics for instance).

Thanks @Pierre Roux , this is much appreciated. Why is this not part of Flocq or similar library?

Would this make sense?

Yes, it should be integrated in Flocq.

Last updated: Oct 04 2023 at 23:01 UTC