Parse a natural number from a string, at some offset.

- Signature
(parse-nat-from-string x val len n xl) → (mv val len)

- Arguments
`x`— The string to parse.

Guard (stringp x) .`val`— Accumulator for the value we have parsed so far; typically 0 to start with.

Guard (natp val) .`len`— Accumulator for the number of digits we have parsed so far; typically 0 to start with.

Guard (natp len) .`n`— Offset intox where we should begin parsing. Must be a valid index into the string, i.e.,0 <= n < (length x) .

Guard (natp n) .`xl`— Pre-computed length ofx .

Guard (eql xl (length x)) .- Returns
`val`— The value of the digits we parsed.

Type (natp val) .`len`— The number of digits we parsed.

Type (natp len) .

This function is flexible but very complicated. See strval for a very simple alternative that may do what you want.

The final

Because of leading zeroes, the

See also parse-nat-from-charlist for a simpler function that reads a number from the start of a character list. This function also serves as part of our logical definition.

**Function: **

(defun parse-nat-from-string (x val len n xl) (declare (xargs :guard (and (stringp x) (natp val) (natp len) (natp n) (eql xl (length x))))) (declare (type string x) (type unsigned-byte val len n xl)) (declare (xargs :split-types t :guard (<= n xl))) (let ((acl2::__function__ 'parse-nat-from-string)) (declare (ignorable acl2::__function__)) (mbe :logic (b* (((mv val len ?rest) (parse-nat-from-charlist (nthcdr n (explode x)) val len))) (mv val len)) :exec (b* (((when (eql n xl)) (mv val len)) ((the (unsigned-byte 8) code) (char-code (the character (char (the string x) (the unsigned-byte n))))) ((unless (and (<= (the (unsigned-byte 8) code) (the (unsigned-byte 8) 57)) (<= (the (unsigned-byte 8) 48) (the (unsigned-byte 8) code)))) (mv val len)) ((the (unsigned-byte 8) dec-digit-char-value) (the (unsigned-byte 8) (- (the (unsigned-byte 8) code) (the (unsigned-byte 8) 48))))) (parse-nat-from-string (the string x) (the unsigned-byte (+ (the (unsigned-byte 8) dec-digit-char-value) (the unsigned-byte (* 10 (the unsigned-byte val))))) (the unsigned-byte (+ 1 (the unsigned-byte len))) (the unsigned-byte (+ 1 (the unsigned-byte n))) (the unsigned-byte xl))))))

**Theorem: **

(defthm natp-of-parse-nat-from-string.val (b* (((mv ?val acl2::?len) (parse-nat-from-string x val len n xl))) (natp val)) :rule-classes :type-prescription)

**Theorem: **

(defthm natp-of-parse-nat-from-string.len (b* (((mv ?val acl2::?len) (parse-nat-from-string x val len n xl))) (natp len)) :rule-classes :type-prescription)