		Search-engine friendly clone of the ACL2 documentation.

Preprocessor

Vl-ppst-unsound-nreverse-acc

Signature
(vl-ppst-unsound-nreverse-acc ppst) → ppst

Definitions and Theorems

Function: vl-ppst-unsound-nreverse-acc

(defun vl-ppst-unsound-nreverse-acc (ppst)
  (declare (xargs :stobjs (ppst)))
  (declare (xargs :guard t))
  (let ((__function__ 'vl-ppst-unsound-nreverse-acc))
    (declare (ignorable __function__))
    (progn$ (raise "Under the hood definition not installed?")
            (b* ((acc (vl-ppst->acc)))
              (vl-ppst-update-acc (rev acc))))))