		Search-engine friendly clone of the ACL2 documentation.

Name-database

Vl-pgenstr-p

(vl-pgenstr-p prefix str) recognizes strings of the form "prefix_n".

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

Definitions and Theorems

Function: vl-pgenstr-p

(defun vl-pgenstr-p (prefix str)
  (declare (xargs :guard (and (stringp prefix) (stringp str))))
  (let ((__function__ 'vl-pgenstr-p))
    (declare (ignorable __function__))
    (b* ((plen (length prefix))
         (slen (length str)))
      (and (< (+ 1 plen) slen)
           (str::strprefixp prefix str)
           (eql (char str plen) #\_)
           (str::dec-digit-string-p-aux str (+ 1 plen)
                                        slen)))))

Theorem: vl-pgenstr-p-of-vl-pgenstr

(defthm vl-pgenstr-p-of-vl-pgenstr
  (implies (and (force (stringp prefix))
                (force (natp n)))
           (vl-pgenstr-p prefix (vl-pgenstr prefix n))))

Theorem: vl-pgenstr-p-of-vl-pgenstr-other

(defthm vl-pgenstr-p-of-vl-pgenstr-other
  (implies (and (not (equal other prefix))
                (force (stringp prefix))
                (force (stringp other)))
           (not (vl-pgenstr-p other (vl-pgenstr prefix n)))))