		Search-engine friendly clone of the ACL2 documentation.

Skip-detection

Sd-pp-problem-header

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

Definitions and Theorems

Function: sd-pp-problem-header-fn

(defun sd-pp-problem-header-fn (x ps)
  (declare (xargs :stobjs (ps)))
  (declare (xargs :guard (sd-problem-p x)))
  (let ((__function__ 'sd-pp-problem-header))
    (declare (ignorable __function__))
    (b* (((sd-problem x) x)
         ((sd-key x.key) x.key)
         (modname (vl-context1->mod x.ctx))
         (htmlp (vl-ps->htmlp)))
      (vl-ps-seq (if htmlp (vl-print-markup "<dt>")
                   (vl-print "  "))
                 (vl-print "Is ")
                 (vl-print-ext-wirename modname x.key.orig)
                 (vl-print " accidentally skipped? ")
                 (vl-ps-span "sd_detail" (vl-print "(score ")
                             (vl-print (sd-problem-score x))
                             (vl-print ", pat ")
                             (vl-print x.key.pat)
                             (vl-print ", priority ")
                             (vl-print x.priority)
                             (vl-print ", groupsize ")
                             (vl-print x.groupsize)
                             (vl-print ")"))
                 (if htmlp (vl-println-markup "</dt>")
                   (vl-println ""))))))