		Search-engine friendly clone of the ACL2 documentation.

Lex-identifiers

Vl-read-simple-identifier

Try to match a simple identifier (or any keyword!).

Signature
(vl-read-simple-identifier echars) → (mv prefix remainder)
Arguments: echars — Guard (vl-echarlist-p echars).

Definitions and Theorems

Function: vl-read-simple-identifier

(defun vl-read-simple-identifier (echars)
  (declare (xargs :guard (vl-echarlist-p echars)))
  (let ((__function__ 'vl-read-simple-identifier))
    (declare (ignorable __function__))
    (if (or (not (consp echars))
            (not (vl-simple-id-head-echar-p (car echars))))
        (mv nil echars)
      (vl-read-while-simple-id-tail echars))))

Theorem: vl-read-simple-identifier-when-vl-simple-id-head-p

(defthm vl-read-simple-identifier-when-vl-simple-id-head-p
  (b* (((mv prefix ?remainder)
        (vl-read-simple-identifier echars)))
    (implies (vl-simple-id-head-p (vl-echar->char (first echars)))
             prefix)))

Subtopics

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