		Search-engine friendly clone of the ACL2 documentation.

Vl-lint

Vl-datatype-svbad-p

Signature
(vl-datatype-svbad-p x) → *
Arguments: x — Guard (vl-datatype-p x).

Definitions and Theorems

Function: vl-datatype-svbad-p

(defun vl-datatype-svbad-p (x)
  (declare (xargs :guard (vl-datatype-p x)))
  (let ((__function__ 'vl-datatype-svbad-p))
    (declare (ignorable __function__))
    (b* (((unless (vl-datatype-resolved-p x)) t)
         ((mv err size) (vl-datatype-size x)))
      (or err
          (and size (> size *vl-svbad-limit*))))))