		Search-engine friendly clone of the ACL2 documentation.

Lex-identifiers

Vl-lex-escaped-identifier

Signature
(vl-lex-escaped-identifier echars breakp) → (mv token/nil remainder)
Arguments: echars — Guard (vl-echarlist-p echars).; breakp — Guard (booleanp breakp).

Per 3.7.2, escaped identifiers cannot be keywords. So we do not need to consult the keyword table.

Definitions and Theorems

Function: vl-lex-escaped-identifier

(defun vl-lex-escaped-identifier (echars breakp)
  (declare (xargs :guard (and (vl-echarlist-p echars)
                              (booleanp breakp))))
  (let ((__function__ 'vl-lex-escaped-identifier))
    (declare (ignorable __function__))
    (b* (((unless (and (consp echars)
                       (eql (vl-echar->char (car echars))
                            #\\)))
          (mv nil echars))
         ((mv name prefix remainder)
          (vl-read-escaped-identifier echars))
         ((unless name)
          (mv (cw "Lexer error (~s0): stray backslash?~%"
                  (vl-location-string (vl-echar->loc (car echars))))
              echars))
         (token (make-vl-idtoken :etext prefix
                                 :name name
                                 :breakp (and breakp t))))
      (mv token remainder))))

Subtopics

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