		Search-engine friendly clone of the ACL2 documentation.

Crypto-hdwallet

String-to-nat

Parse a string into a natural number.

Signature
(string-to-nat string) → (mv error? nat)
Arguments: string — Guard (stringp string).
Returns: error? — Type (booleanp error?).; nat — Type (natp nat).

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 t.

Definitions and Theorems

Function: string-to-nat

(defun string-to-nat (string)
  (declare (xargs :guard (stringp string)))
  (b* ((val (strval string))
       ((when (null val)) (mv t 0)))
    (mv nil val)))

Theorem: booleanp-of-string-to-nat.error?

(defthm booleanp-of-string-to-nat.error?
  (b* (((mv ?error? acl2::?nat)
        (string-to-nat string)))
    (booleanp error?))
  :rule-classes :rewrite)

Theorem: natp-of-string-to-nat.nat

(defthm natp-of-string-to-nat.nat
  (b* (((mv ?error? acl2::?nat)
        (string-to-nat string)))
    (natp nat))
  :rule-classes :rewrite)