Ensure that a function's inputs are simple enough to convert into nets.
(vl-portdecllist-types-okp x warnings function) → (mv okp warnings)
Function:
(defun vl-portdecllist-types-okp (x warnings function) (declare (xargs :guard (and (vl-portdecllist-p x) (vl-warninglist-p warnings) (vl-fundecl-p function)))) (let ((__function__ 'vl-portdecllist-types-okp)) (declare (ignorable __function__)) (b* (((when (atom x)) (mv t (ok))) ((vl-portdecl x1) (car x)) ((unless (and (eq (vl-datatype-kind x1.type) :vl-coretype) (member (vl-coretype->name x1.type) '(:vl-logic :vl-reg)))) (mv nil (fatal :type :vl-bad-function-input :msg "In ~a0, input ~s1 has unsupported type ~s2." :args (list function x1.name x1.type))))) (vl-portdecllist-types-okp (cdr x) warnings function))))
Theorem:
(defthm booleanp-of-vl-portdecllist-types-okp.okp (b* (((mv ?okp ?warnings) (vl-portdecllist-types-okp x warnings function))) (booleanp okp)) :rule-classes :type-prescription)
Theorem:
(defthm vl-warninglist-p-of-vl-portdecllist-types-okp.warnings (b* (((mv ?okp ?warnings) (vl-portdecllist-types-okp x warnings function))) (vl-warninglist-p warnings)) :rule-classes :rewrite)