Zulip Chat Archive
Stream: lean4
Topic: Parse Nat from String
Cole Shepherd (Dec 02 2022 at 01:14):
How do you parse a Nat from a String?
Alex J. Best (Dec 02 2022 at 01:23):
You can use docs4#String.toNat! or docs4#String.toNat? depending on what behaviour you want
Last updated: Dec 20 2023 at 11:08 UTC