		Search-engine friendly clone of the ACL2 documentation.

Hid-tools

Vl-selstep-usertypes-ok

Signature
(vl-selstep-usertypes-ok x) → *
Arguments: x — Guard (vl-selstep-p x).

Definitions and Theorems

Function: vl-selstep-usertypes-ok

(defun vl-selstep-usertypes-ok (x)
  (declare (xargs :guard (vl-selstep-p x)))
  (let ((__function__ 'vl-selstep-usertypes-ok))
    (declare (ignorable __function__))
    (b* (((vl-selstep x)))
      (vl-datatype-resolved-p x.type))))

Theorem: vl-selstep-usertypes-ok-of-vl-selstep-fix-x

(defthm vl-selstep-usertypes-ok-of-vl-selstep-fix-x
  (equal (vl-selstep-usertypes-ok (vl-selstep-fix x))
         (vl-selstep-usertypes-ok x)))

Theorem: vl-selstep-usertypes-ok-vl-selstep-equiv-congruence-on-x

(defthm vl-selstep-usertypes-ok-vl-selstep-equiv-congruence-on-x
  (implies (vl-selstep-equiv x x-equiv)
           (equal (vl-selstep-usertypes-ok x)
                  (vl-selstep-usertypes-ok x-equiv)))
  :rule-classes :congruence)