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: May 02 2025 at 03:31 UTC