Get the kind field from a vl-basictype.
(vl-basictype->kind x) → kind
This is an ordinary field accessor created by defprod.
Function:
(defun vl-basictype->kind$inline (x) (declare (xargs :guard (vl-basictype-p x))) (declare (xargs :guard t)) (let ((__function__ 'vl-basictype->kind)) (declare (ignorable __function__)) (mbe :logic (b* ((x (and t x))) (vl-basictypekind-fix (cdr x))) :exec (cdr x))))
Theorem:
(defthm vl-basictypekind-p-of-vl-basictype->kind (b* ((kind (vl-basictype->kind$inline x))) (vl-basictypekind-p kind)) :rule-classes :rewrite)
Theorem:
(defthm vl-basictype->kind$inline-of-vl-basictype-fix-x (equal (vl-basictype->kind$inline (vl-basictype-fix x)) (vl-basictype->kind$inline x)))
Theorem:
(defthm vl-basictype->kind$inline-vl-basictype-equiv-congruence-on-x (implies (vl-basictype-equiv x x-equiv) (equal (vl-basictype->kind$inline x) (vl-basictype->kind$inline x-equiv))) :rule-classes :congruence)