		Search-engine friendly clone of the ACL2 documentation.

Vl-lint

Sd-problem-major-p

Signature
(sd-problem-major-p x) → *
Arguments: x — Guard (sd-problem-p x).

Definitions and Theorems

Function: sd-problem-major-p

(defun sd-problem-major-p (x)
  (declare (xargs :guard (sd-problem-p x)))
  (let ((__function__ 'sd-problem-major-p))
    (declare (ignorable __function__))
    (b* (((sd-problem x) x))
      (or (>= x.priority 10)
          (and (>= x.priority 6)
               (>= x.groupsize 4))
          (>= (sd-problem-score x) 8)))))