		Search-engine friendly clone of the ACL2 documentation.

Lexer-utils

Vl-read-some-literal

Match one of many exact literal strings.

Signature
(vl-read-some-literal strings echars) → (mv prefix remainder)
Arguments: strings — The strings to search for, in priority order.
Guard (string-listp strings).; 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-some-literal

(defun vl-read-some-literal (strings echars)
  (declare (xargs :guard (and (string-listp strings)
                              (vl-echarlist-p echars))))
  (declare (xargs :guard (not (member-equal "" strings))))
  (let ((__function__ 'vl-read-some-literal))
    (declare (ignorable __function__))
    (b* (((when (atom strings)) (mv nil echars))
         ((mv prefix remainder)
          (vl-read-literal (car strings) echars))
         ((when prefix) (mv prefix remainder)))
      (vl-read-some-literal (cdr strings)
                            echars))))

Subtopics

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