		Search-engine friendly clone of the ACL2 documentation.

Vl-read-until-literal

Vl-read-until-literal-impl

Signature
(vl-read-until-literal-impl string echars acc) → (mv * * *)
Arguments: echars — Guard (vl-echarlist-p echars).

Definitions and Theorems

Function: vl-read-until-literal-impl

(defun vl-read-until-literal-impl (string echars acc)
 (declare (type string string))
 (declare (xargs :guard (vl-echarlist-p echars)))
 (declare (xargs :guard (not (equal string ""))))
 (let ((__function__ 'vl-read-until-literal-impl))
   (declare (ignorable __function__))
   (cond ((atom echars) (mv nil acc echars))
         ((vl-matches-string-p string echars)
          (mv t acc echars))
         (t (vl-read-until-literal-impl string (cdr echars)
                                        (cons (car echars) acc))))))