		Search-engine friendly clone of the ACL2 documentation.

Oddexpr-check

Vl-pp-oddexpr-details

Signature
(vl-pp-oddexpr-details x &key (ps 'ps)) → ps

Definitions and Theorems

Function: vl-pp-oddexpr-details-fn

(defun vl-pp-oddexpr-details-fn (x ps)
  (declare (xargs :stobjs (ps)))
  (declare (xargs :guard t))
  (let ((__function__ 'vl-pp-oddexpr-details))
    (declare (ignorable __function__))
    (cond ((atom x) ps)
          ((atom (car x))
           (prog2$ (raise "Bad details: ~x0~%" x)
                   ps))
          (t (vl-ps-seq (vl-print "     - ")
                        (vl-cw "~s0: ~a1~%" (caar x) (cdar x))
                        (vl-pp-oddexpr-details (cdr x)))))))