Zulip Chat Archive

Stream: general

Topic: String to Float


Charles Hughes (Sep 21 2021 at 06:28):

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

Charles Hughes (Sep 21 2021 at 06:30):

I see a toString for Float but no ofString

Charles Hughes (Sep 21 2021 at 06:31):

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

Eric Wieser (Sep 21 2021 at 07:03):

Are you asking about #lean4?

Notification Bot (Sep 21 2021 at 08:00):

This topic was moved by Sebastian Ullrich to #lean4 > String to Float


Last updated: Dec 20 2023 at 11:08 UTC