		Search-engine friendly clone of the ACL2 documentation.

Preprocessor

Vl-ppst->acc

Signature
(vl-ppst->acc &key (ppst 'ppst)) → acc
Returns: acc — Type (vl-echarlist-p acc).

Definitions and Theorems

Function: vl-ppst->acc$inline

(defun vl-ppst->acc$inline (ppst)
  (declare (xargs :stobjs (ppst)))
  (declare (xargs :guard t))
  (let ((__function__ 'vl-ppst->acc))
    (declare (ignorable __function__))
    (mbe :logic (vl-echarlist-fix (vl-ppst->acc-raw ppst))
         :exec (vl-ppst->acc-raw ppst))))

Theorem: vl-echarlist-p-of-vl-ppst->acc

(defthm vl-echarlist-p-of-vl-ppst->acc
  (b* ((acc (vl-ppst->acc$inline ppst)))
    (vl-echarlist-p acc))
  :rule-classes :rewrite)