float('3.3') in Lean 4?

Stream: Is there code for X?

[Anders Larsson]

In Python I can do:

>>> float('3.3')
3.3

How do i go from String to Float in Lean 4?

[Jireh Loreaux]

Lean has docs#OfScientific class which allows decimal notation to be interpreted as a term of the relevant type. There should already be an instance (docs#instOfScientificFloat) for docs#Float. Now, if you actually want to get there from a string, you would need a parser to convert the string into syntax. I'm not sure where that is off-hand though.

But #check 3.3 : Float works out of the box. In fact, the type annotation here is unnecessary because this is the default instance.

[Adam Topaz]

Do we not have docs#String.toFloat?

[Adam Topaz]

Hmmm I guess not, although we have docs#String.toNat?

[Anders Larsson]

Not that I can find. But the Lean parser itself obviously can parse 3.3. So the code exists (If that code isn't hidden in the C++ parts).

[Jireh Loreaux]

Yes, I know it can, I just don't know where it is. :sweat_smile:

[Anders Larsson]

I managed to do a work around (by using ns : Nat instead of seconds : Float ).

But I'm still interested to know if I missed something obvious.

[Jireh Loreaux]

Can you provide an #mwe?

[Eric Wieser]

Anders Larsson said:

I managed to do a work around (by using ns : Nat instead of seconds : Float ).

But I'm still interested to know if I missed something obvious.

This is probably the right approach anyway because Float is worse and worse at representing nanoseconds away from 0

[Adam Topaz]

You could parse the string as a docs#Lean.JsonNumber and get to float from there

[Adam Topaz]

Using docs#Lean.JsonNumber.toFloat

[Adam Topaz]

Use docs#Lean.Json.parseJson? to parse as json

[Adam Topaz]

Hmmm… we have parseJson somewhere but I can’t seem to find it now

[Adam Topaz]

Oh it’s just docs#Lean.Json.parse

[Adam Topaz]

I was bored at the Toronto airport...

import Lean.Data.Json.Parser

def parseFloat (s : String) : Except String Float :=
  match Lean.Json.parse s with
    | .ok (.num t) => .ok t.toFloat
    | _ => throw "Failed to parse as float."

#eval parseFloat "25.123651"