		Search-engine friendly clone of the ACL2 documentation.

Ps-macros

Vl-ps->rchars

This is misnamed for historic reasons. It used to return a character list in reverse order. It now returns a vl-printedlist-p, also in reverse order.

Macro: vl-ps->rchars

(defmacro vl-ps->rchars nil
  '(vl-ps->rchars-fn ps))

Definitions and Theorems

Function: vl-ps->rchars-fn$inline

(defun vl-ps->rchars-fn$inline (ps)
  (declare (xargs :stobjs (ps)))
  (declare (xargs :guard t))
  (let ((__function__ 'vl-ps->rchars-fn))
    (declare (ignorable __function__))
    (mbe :logic
         (let ((rchars (vl-ps->rchars-raw ps)))
           (if (vl-printedlist-p rchars)
               rchars
             nil))
         :exec (vl-ps->rchars-raw ps))))

Theorem: vl-printedlist-p-of-vl-ps->rchars-fn

(defthm vl-printedlist-p-of-vl-ps->rchars-fn
  (b* ((rchars (vl-ps->rchars-fn$inline ps)))
    (vl-printedlist-p rchars))
  :rule-classes :rewrite)