		Search-engine friendly clone of the ACL2 documentation.

Name-database

Vl-pgenstr->val

(vl-pgenstr->val prefix str) retrieves n from the string str, which must have the form "prefix_n"; we return n as a natural number.

Signature
(vl-pgenstr->val prefix str) → *
Arguments: prefix — Guard (stringp prefix).; str — Guard (stringp str).

Definitions and Theorems

Function: vl-pgenstr->val

(defun vl-pgenstr->val (prefix str)
  (declare (xargs :guard (and (stringp prefix) (stringp str))))
  (declare (xargs :guard (vl-pgenstr-p prefix str)))
  (let ((__function__ 'vl-pgenstr->val))
    (declare (ignorable __function__))
    (b* (((mv val ?len)
          (str::parse-nat-from-string str 0 0 (+ 1 (length prefix))
                                      (length str))))
      (lnfix val))))

Theorem: vl-pgenstr->val-of-vl-pgenstr

(defthm vl-pgenstr->val-of-vl-pgenstr
  (implies (and (force (stringp prefix))
                (force (natp n)))
           (equal (vl-pgenstr->val prefix (vl-pgenstr prefix n))
                  n)))