(vl-simpletype-p x) → *
Function:
(defun vl-simpletype-p (x) (declare (xargs :guard (vl-datatype-p x))) (let ((__function__ 'vl-simpletype-p)) (declare (ignorable __function__)) (vl-datatype-case x :vl-coretype (and (or (eq x.name :vl-reg) (eq x.name :vl-logic)) (atom x.udims) (or (atom x.pdims) (and (atom (cdr x.pdims)) (mbe :logic (vl-range-p (car x.pdims)) :exec (not (eq (car x.pdims) :vl-unsized-dimension)))))) :otherwise nil)))
Theorem:
(defthm vl-simpletype-p-of-vl-datatype-fix-x (equal (vl-simpletype-p (vl-datatype-fix x)) (vl-simpletype-p x)))
Theorem:
(defthm vl-simpletype-p-vl-datatype-equiv-congruence-on-x (implies (vl-datatype-equiv x x-equiv) (equal (vl-simpletype-p x) (vl-simpletype-p x-equiv))) :rule-classes :congruence)