		Search-engine friendly clone of the ACL2 documentation.

Skip-detection

Sd-pp-problemlist-brief

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

Definitions and Theorems

Function: sd-pp-problemlist-brief-fn

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