Find the first non-
(vl-portdecllist-find-noninput x) → decl?
Function:
(defun vl-portdecllist-find-noninput (x) (declare (xargs :guard (vl-portdecllist-p x))) (let ((__function__ 'vl-portdecllist-find-noninput)) (declare (ignorable __function__)) (cond ((atom x) nil) ((eq (vl-portdecl->dir (car x)) :vl-input) (vl-portdecllist-find-noninput (cdr x))) (t (vl-portdecl-fix (car x))))))
Theorem:
(defthm return-type-of-vl-portdecllist-find-noninput (b* ((decl? (vl-portdecllist-find-noninput x))) (equal (vl-portdecl-p decl?) (if decl? t nil))) :rule-classes :rewrite)