		Search-engine friendly clone of the ACL2 documentation.

Portdecl-sign

Vl-datatype->signedp

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

Definitions and Theorems

Function: vl-datatype->signedp

(defun vl-datatype->signedp (x)
  (declare (xargs :guard (vl-datatype-p x)))
  (let ((__function__ 'vl-datatype->signedp))
    (declare (ignorable __function__))
    (vl-datatype-case x
                      :vl-coretype x.signedp
                      :vl-struct x.signedp
                      :vl-union x.signedp
                      :otherwise nil)))

Theorem: vl-datatype->signedp-of-vl-datatype-fix-x

(defthm vl-datatype->signedp-of-vl-datatype-fix-x
  (equal (vl-datatype->signedp (vl-datatype-fix x))
         (vl-datatype->signedp x)))

Theorem: vl-datatype->signedp-vl-datatype-equiv-congruence-on-x

(defthm vl-datatype->signedp-vl-datatype-equiv-congruence-on-x
  (implies (vl-datatype-equiv x x-equiv)
           (equal (vl-datatype->signedp x)
                  (vl-datatype->signedp x-equiv)))
  :rule-classes :congruence)