		Search-engine friendly clone of the ACL2 documentation.

Lex-identifiers

Vl-read-escaped-identifier

Signature
(vl-read-escaped-identifier echars) → (mv name/nil prefix remainder)
Arguments: echars — Guard (vl-echarlist-p echars).
Returns: name/nil — On success, a string with the interpreted name (similar to prefix, but without the leading backslash or trailing whitespace character.).
Type (equal (stringp name/nil) (if name/nil t nil)), given the guard.

Definitions and Theorems

Function: vl-read-escaped-identifier

(defun vl-read-escaped-identifier (echars)
  (declare (xargs :guard (vl-echarlist-p echars)))
  (let ((__function__ 'vl-read-escaped-identifier))
    (declare (ignorable __function__))
    (b* (((when (or (not (consp echars))
                    (not (eql (vl-echar->char (car echars))
                              #\\))))
          (mv nil nil echars))
         ((mv tail remainder)
          (vl-read-while-printable-not-whitespace (cdr echars)))
         ((unless tail) (mv nil nil echars))
         ((unless (consp remainder))
          (mv (hons-copy (vl-echarlist->string tail))
              (cons (car echars) tail)
              remainder)))
      (mv (hons-copy (vl-echarlist->string tail))
          (cons (car echars)
                (append tail (list (car remainder))))
          (cdr remainder)))))

Theorem: return-type-of-vl-read-escaped-identifier.name/nil

(defthm return-type-of-vl-read-escaped-identifier.name/nil
  (implies (and (force (vl-echarlist-p echars)))
           (b* (((mv ?name/nil ?prefix ?remainder)
                 (vl-read-escaped-identifier echars)))
             (equal (stringp name/nil)
                    (if name/nil t nil))))
  :rule-classes :rewrite)

Theorem: vl-read-escaped-identifier-under-iff

(defthm vl-read-escaped-identifier-under-iff
  (b* (((mv name prefix ?remainder)
        (vl-read-escaped-identifier echars)))
    (iff prefix name)))

Subtopics

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