		Search-engine friendly clone of the ACL2 documentation.

Preprocessor

Vl-ppst->bytes

Signature
(vl-ppst->bytes &key (ppst 'ppst)) → bytes
Returns: bytes — Type (natp bytes).

Definitions and Theorems

Function: vl-ppst->bytes$inline

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

Theorem: natp-of-vl-ppst->bytes

(defthm natp-of-vl-ppst->bytes
  (b* ((bytes (vl-ppst->bytes$inline ppst)))
    (natp bytes))
  :rule-classes :rewrite)