		Search-engine friendly clone of the ACL2 documentation.

Preprocessor

Vl-atvl-atts-text

Signature
(vl-atvl-atts-text echars) → (mv atts-text remainder)
Arguments: echars — Guard (vl-echarlist-p echars).
Returns: atts-text — Type (vl-echarlist-p atts-text).; remainder — Type (vl-echarlist-p remainder).

Definitions and Theorems

Function: vl-atvl-atts-text

(defun vl-atvl-atts-text (echars)
  (declare (xargs :guard (vl-echarlist-p echars)))
  (let ((__function__ 'vl-atvl-atts-text))
    (declare (ignorable __function__))
    (b* ((echars (vl-echarlist-fix echars))
         ((mv & prefix remainder)
          (vl-read-until-literal *nls* (rest-n 5 echars)))
         ((mv comment1p pre-comment1 post-comment1)
          (vl-read-until-literal "//" prefix))
         ((mv comment2p pre-comment2 post-comment2)
          (vl-read-until-literal "/*" prefix)))
      (cond ((acl2::and** comment1p comment2p)
             (if (< (len pre-comment1)
                    (len pre-comment2))
                 (mv pre-comment1
                     (append post-comment1 remainder))
               (mv pre-comment2
                   (append post-comment2 remainder))))
            (comment1p (mv pre-comment1
                           (append post-comment1 remainder)))
            (comment2p (mv pre-comment2
                           (append post-comment2 remainder)))
            (t (mv prefix remainder))))))

Theorem: vl-echarlist-p-of-vl-atvl-atts-text.atts-text

(defthm vl-echarlist-p-of-vl-atvl-atts-text.atts-text
  (b* (((mv ?atts-text ?remainder)
        (vl-atvl-atts-text echars)))
    (vl-echarlist-p atts-text))
  :rule-classes :rewrite)

Theorem: vl-echarlist-p-of-vl-atvl-atts-text.remainder

(defthm vl-echarlist-p-of-vl-atvl-atts-text.remainder
  (b* (((mv ?atts-text ?remainder)
        (vl-atvl-atts-text echars)))
    (vl-echarlist-p remainder))
  :rule-classes :rewrite)

Theorem: true-listp-atts-text-of-vl-atvl-atts-text

(defthm true-listp-atts-text-of-vl-atvl-atts-text
  (b* (((mv ?atts-text ?remainder)
        (vl-atvl-atts-text echars)))
    (true-listp atts-text))
  :rule-classes :type-prescription)