(vl-interpret-expr-as-type x) → type
Function:
(defun vl-interpret-expr-as-type (x) (declare (xargs :guard (vl-expr-p x))) (let ((__function__ 'vl-interpret-expr-as-type)) (declare (ignorable __function__)) (vl-expr-case x :vl-index (and (atom x.indices) (vl-partselect-case x.part :none) (make-vl-usertype :name x.scope)) :otherwise nil)))
Theorem:
(defthm vl-maybe-datatype-p-of-vl-interpret-expr-as-type (b* ((type (vl-interpret-expr-as-type x))) (vl-maybe-datatype-p type)) :rule-classes :rewrite)