		Search-engine friendly clone of the ACL2 documentation.

Ps-macros

Vl-ps->autowrap-col

Macro: vl-ps->autowrap-col

(defmacro vl-ps->autowrap-col nil
  '(vl-ps->autowrap-col-fn ps))

Definitions and Theorems

Function: vl-ps->autowrap-col-fn$inline

(defun vl-ps->autowrap-col-fn$inline (ps)
  (declare (xargs :stobjs (ps)))
  (declare (xargs :guard t))
  (let ((__function__ 'vl-ps->autowrap-col-fn))
    (declare (ignorable __function__))
    (mbe :logic (nfix (vl-ps->autowrap-col-raw ps))
         :exec (vl-ps->autowrap-col-raw ps))))

Theorem: natp-of-vl-ps->autowrap-col-fn

(defthm natp-of-vl-ps->autowrap-col-fn
  (b* ((autowrap-col (vl-ps->autowrap-col-fn$inline ps)))
    (natp autowrap-col))
  :rule-classes :type-prescription)