		Search-engine friendly clone of the ACL2 documentation.

Skip-detection

Sd-pp-problem-brief

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

Definitions and Theorems

Function: sd-pp-problem-brief-fn

(defun sd-pp-problem-brief-fn (x ps)
 (declare (xargs :stobjs (ps)))
 (declare (xargs :guard (sd-problem-p x)))
 (let ((__function__ 'sd-pp-problem-brief))
  (declare (ignorable __function__))
  (b* (((sd-problem x) x)
       (htmlp (vl-ps->htmlp)))
    (vl-ps-seq (sd-pp-problem-header x)
               (if htmlp (vl-print-markup "<dd class=\"sd_context\">")
                 (vl-indent 2))
               (vl-println (vl-context-summary x.ctx))
               (if htmlp (vl-println-markup "</dd>")
                 (vl-println ""))))))