		Search-engine friendly clone of the ACL2 documentation.

Lex-strings

Vl-lex-string

Lexing of string literals.

Signature
(vl-lex-string echars st) → (mv token/nil remainder)
Arguments: echars — Guard (vl-echarlist-p echars).; st — Guard (vl-lexstate-p st).

Definitions and Theorems

Function: vl-lex-string

(defun vl-lex-string (echars st)
  (declare (xargs :guard (and (vl-echarlist-p echars)
                              (vl-lexstate-p st))))
  (let ((__function__ 'vl-lex-string))
    (declare (ignorable __function__))
    (b* (((unless (and (consp echars)
                       (eql (vl-echar->char (car echars))
                            #\")))
          (mv nil echars))
         ((mv string prefix remainder)
          (vl-read-string echars st))
         ((unless string) (mv nil echars))
         (token (make-vl-stringtoken :etext prefix
                                     :expansion string)))
      (mv token remainder))))

Subtopics

Vl-lex-string-token/remainder-thms: Token and remainder theorems for vl-lex-string, automatically generated by def-token/remainder-thms.