		Search-engine friendly clone of the ACL2 documentation.

Vl-matches-string-p

Vl-matches-string-p-impl

Signature
(vl-matches-string-p-impl string i len echars) → *
Arguments: len — Guard (equal len (length string)).; echars — Guard (vl-echarlist-p echars).

Definitions and Theorems

Function: vl-matches-string-p-impl

(defun vl-matches-string-p-impl (string i len echars)
 (declare (type string string)
          (type unsigned-byte i))
 (declare (xargs :guard (and (vl-echarlist-p echars)
                             (equal len (length string)))))
 (let ((__function__ 'vl-matches-string-p-impl))
  (declare (ignorable __function__))
  (mbe
     :logic (or (>= (nfix i) (nfix len))
                (and (consp echars)
                     (eql (char string i)
                          (vl-echar->char (car echars)))
                     (vl-matches-string-p-impl string (+ (nfix i) 1)
                                               len (cdr echars))))
     :exec (or (>= i len)
               (and (consp echars)
                    (eql (char string i)
                         (the character
                              (vl-echar->char (car echars))))
                    (vl-matches-string-p-impl string (+ i 1)
                                              len (cdr echars)))))))