Parse a string into a natural number.
Certain wallet commands take natural numbers as inputs,
which are supplied by the wallet's user as strings.
These must be non-empty sequences of decimal digits,
which are turned into their big-endian value.
If the string cannot be converted to a natural number,
the error result is
(defun string-to-nat (string) (declare (xargs :guard (stringp string))) (b* ((val (strval string)) ((when (null val)) (mv t 0))) (mv nil val)))
(defthm booleanp-of-string-to-nat.error? (b* (((mv ?error? acl2::?nat) (string-to-nat string))) (booleanp error?)) :rule-classes :rewrite)
(defthm natp-of-string-to-nat.nat (b* (((mv ?error? acl2::?nat) (string-to-nat string))) (natp nat)) :rule-classes :rewrite)