Zulip Chat Archive

Stream: lean4

Topic: printing floats


Arthur Paulino (Apr 30 2022 at 00:17):

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 (Apr 30 2022 at 00:33):

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 (Apr 30 2022 at 00:37):

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

Leonardo de Moura (Apr 30 2022 at 00:51):

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


Last updated: Dec 20 2023 at 11:08 UTC