printing floats

Stream: lean4

[Arthur Paulino]

I've been meaning to ask this question for a while, but why are Float numbers printed with extra zeros in the right? I always have to clean it up with a function like this before printing floats

def removeRightmostZeros (s : String) : String :=
  let rec aux (buff res : List Char) : List Char → List Char
    | []      => res.reverse
    | a :: as =>
      if a != '0'
        then aux [] (a :: (buff ++ res)) as
        else aux (a :: buff) res as
  ⟨aux [] [] s.data⟩

#eval 1.4                                 -- 1.400000
#eval (toString 1.4)                      -- "1.400000"
#eval removeRightmostZeros (toString 1.4) -- "1.4"

[Leonardo de Moura]

The Float to String is implemented in the runtime

extern "C" LEAN_EXPORT lean_obj_res lean_float_to_string(double a) {
    return mk_string(std::to_string(a));
}

The function std::to_string is from the C++ standard library. It would be great to replace it with something better.

[Arthur Paulino]

I see, thanks!
What do you mean by "better" in this case? Something else besides cleaning these trailing zeros?

[Leonardo de Moura]

"better" = "use the same approach used in languages like Haskell or Rust" :)