(vl-port/vardecllist-p x) recognizes lists where every element satisfies vl-port/vardecl-p.
(vl-port/vardecllist-p x) → std::bool
This is an ordinary deflist. It is
"loose" in that it does not care whether
Function:
(defun vl-port/vardecllist-p (x) (declare (xargs :guard t)) (let ((__function__ 'vl-port/vardecllist-p)) (declare (ignorable __function__)) (if (consp x) (and (vl-port/vardecl-p (car x)) (vl-port/vardecllist-p (cdr x))) t)))
Theorem:
(defthm vl-port/vardecllist-p-when-vl-portdecllist-p (implies (vl-portdecllist-p x) (vl-port/vardecllist-p x)))
Theorem:
(defthm vl-port/vardecllist-p-when-vl-vardecllist-p (implies (vl-vardecllist-p x) (vl-port/vardecllist-p x)))