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