(vl-erangetypelist-p x) recognizes lists where every element satisfies vl-erangetype-p.
(vl-erangetypelist-p x) → std::bool
This is an ordinary deflist. It is
"loose" in that it does not care whether
Function:
(defun vl-erangetypelist-p (x) (declare (xargs :guard t)) (let ((__function__ 'vl-erangetypelist-p)) (declare (ignorable __function__)) (if (consp x) (and (vl-erangetype-p (car x)) (vl-erangetypelist-p (cdr x))) t)))
Theorem:
(defthm vl-erangetype-p-of-vl-type-of-matched-token (implies (vl-erangetypelist-p types) (equal (vl-erangetype-p (vl-type-of-matched-token types tokens)) (if (vl-type-of-matched-token types tokens) t nil))))