String to Float

Stream: lean4

[Charles Hughes]

Is there some way to convert a String to a Float? I'm trying to take Floats as inputs to my binary

[Charles Hughes]

I see a toString for Float but no ofString

[Charles Hughes]

hm maybe passing the values via sci notation would be the easiest

[Eric Wieser]

Are you asking about #lean4?

[Charles Hughes]

yes

[Notification Bot]

This topic was moved here from #general > String to Float by Sebastian Ullrich

[Christian Pehle]

(deleted)

[Siddhartha Gadgil]

There are a couple of methods in Meta which may help: there is decodeScientificLitVal?which gives components and the typeclass OfScientific that has a float instance.

[Siddhartha Gadgil]

Here is an example:

def getFloat (s: String) : Option Float :=
  (Syntax.decodeScientificLitVal? s).map (fun ⟨m, s, e⟩ => Float.ofScientific m s e)

#eval getFloat "3.1415" -- gives some 3.141500

[Mac]

Here is a somewhat hacky solution that none-the-less gets the job done:

import Lean.Data.Json.Parser

open Lean in
def parse (s : String) : Except String Float :=
  match Json.Parser.num s.mkIterator with
  | Parsec.ParseResult.success _ res =>
    Except.ok <| Float.ofInt res.mantissa * 10 ^ - Float.ofNat res.exponent
  | Parsec.ParseResult.error it err  => Except.error s!"offset {it.i.repr}: {err}"

#eval parse "1.3" -- Except.ok 1.300000

[Charles Hughes]

Thanks Mac!