I need to parse a Float from a typical decimal floating point String in my Lean program (e.g. 3.14), but there does not seem to be any standard library facilities for this. There is String.toNat for Nat, and a series of similar functions--none of these seem to work on Float. If this functionality does not exist in the standard library, is there an (ideally, popular) external library that I can leverage?

If neither of these are feasible...what's my best option? Call the Lean parser? FFI and call strtod from the C standard library? Implement it by hand?