ToJson Float is missing?

Stream: lean4

[Chris Lovett]

How do I create JSon containing a floating point number? Float seems to be entirely missing from fromtojson.lean even though JsonNumber contains a mantissa and exponent...? (although the JSonNumber might also be missing an exponentSign). Am I missing something?

And how do I "round" a Float to an integer? (Float.ceil, Float.round, Float.floor seem to be missing?)

[Marc Huisinga]

JsonNumber is a decimal float (converting between decimal and binary floats is lossy, so you want to delay it for as long as possible). The exponent sign is not missing, it's just a normalized representation (x*10^n = (10^n*x)*10^(-0) for n > 0).
A Float -> JsonNumber function does indeed seem to be missing. That part of the library was written for the server before Lean 4 had a workable float API. It would probably need to be implemented via C++. Unfortunately, this type of stuff is always very fiddly and hard to get fully right ... (Possible reference implementation: https://github.com/google/double-conversion)

JsonNumber -> Float is already easy thanks to OfScientific:

def toFloat (jn : JsonNumber) : Float :=
  let sign := if jn.mantissa < 0 then -1 else 1
  sign*OfScientific.ofScientific jn.mantissa.natAbs true jn.exponent

Rounding should probably also be exposed from C++.

[Leonardo de Moura]

I exposed the C rounding functions.
https://github.com/leanprover/lean4/commit/5294a39ec4e0d4b1e023d3f981696c540e5492e2

[Eric Wieser]

Note that the lean3 versions of these functions (docs#native.float.round etc) have a different signature to the Lean4 ones