		Search-engine friendly clone of the ACL2 documentation.

Lex-identifiers

Vl-lex-escaped-identifier

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

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)
  (declare (xargs :guard (vl-echarlist-p echars)))
  (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)))
      (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.