(vl-basictype->datatype x) → (mv warning type)
Function:
(defun vl-basictype->datatype (x) (declare (xargs :guard (vl-basictypekind-p x))) (let ((__function__ 'vl-basictype->datatype)) (declare (ignorable __function__)) (b* ((x (vl-basictypekind-fix x)) ((when (vl-coretypename-p x)) (mv nil (make-vl-coretype :name x)))) (mv (make-vl-warning :type :vl-basictype->datatype-fail :msg "Couldn't resolve type of ~a0." :args (list x)) nil))))
Theorem:
(defthm return-type-of-vl-basictype->datatype.warning (b* (((mv common-lisp::?warning common-lisp::?type) (vl-basictype->datatype x))) (iff (vl-warning-p warning) warning)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-vl-basictype->datatype.type (b* (((mv common-lisp::?warning common-lisp::?type) (vl-basictype->datatype x))) (implies (not warning) (vl-datatype-p type))) :rule-classes :rewrite)
Theorem:
(defthm vl-basictype->datatype-of-vl-basictypekind-fix-x (equal (vl-basictype->datatype (vl-basictypekind-fix x)) (vl-basictype->datatype x)))
Theorem:
(defthm vl-basictype->datatype-vl-basictypekind-equiv-congruence-on-x (implies (vl-basictypekind-equiv x x-equiv) (equal (vl-basictype->datatype x) (vl-basictype->datatype x-equiv))) :rule-classes :congruence)