		Search-engine friendly clone of the ACL2 documentation.

Preprocessor

Vl-ppst->defines

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

Definitions and Theorems

Function: vl-ppst->defines$inline

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

Theorem: vl-defines-p-of-vl-ppst->defines

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