		Search-engine friendly clone of the ACL2 documentation.

Skip-detection

Sd-pp-problemlist-long

Signature
(sd-pp-problemlist-long x &key (ps 'ps)) → ps
Arguments: x — Guard (sd-problemlist-p x).

Definitions and Theorems

Function: sd-pp-problemlist-long-fn

(defun sd-pp-problemlist-long-fn (x ps)
  (declare (xargs :stobjs (ps)))
  (declare (xargs :guard (sd-problemlist-p x)))
  (let ((__function__ 'sd-pp-problemlist-long))
    (declare (ignorable __function__))
    (if (atom x)
        ps
      (vl-ps-seq (sd-pp-problem-long (car x))
                 (sd-pp-problemlist-long (cdr x))))))