		Search-engine friendly clone of the ACL2 documentation.

Lexer-utils

Vl-read-literal

Match an exact literal string.

Signature
(vl-read-literal string echars) → (mv prefix remainder)
Arguments: string — The string we're looking for.; echars — The characters we're lexing.
Guard (vl-echarlist-p echars).
Returns: prefix — nil on failure, or the matching prefix of echars on success.

Definitions and Theorems

Function: vl-read-literal$inline

(defun vl-read-literal$inline (string echars)
  (declare (type string string))
  (declare (xargs :guard (vl-echarlist-p echars)))
  (declare (xargs :guard (not (equal string ""))))
  (let ((__function__ 'vl-read-literal))
    (declare (ignorable __function__))
    (if (vl-matches-string-p string echars)
        (let ((strlen (length (string-fix string))))
          (mv (first-n strlen echars)
              (rest-n strlen echars)))
      (mv nil echars))))

Theorem: vl-echarlist->chars-of-prefix-of-vl-read-literal

(defthm vl-echarlist->chars-of-prefix-of-vl-read-literal
  (b* (((mv prefix ?remainder)
        (vl-read-literal string echars)))
    (implies prefix
             (equal (vl-echarlist->chars prefix)
                    (explode string)))))

Theorem: vl-echarlist->string-of-prefix-of-vl-read-literal

(defthm vl-echarlist->string-of-prefix-of-vl-read-literal
  (b* (((mv prefix ?remainder)
        (vl-read-literal string echars)))
    (implies prefix
             (equal (vl-echarlist->string prefix)
                    (string-fix string)))))

Subtopics

Vl-read-literal-prefix/remainder-thms: Prefix and remainder theorems for vl-read-literal, automatically generated by def-prefix/remainder-thms.