(sv::maybe-modnamelist-p x) → *
Function:
(defun sv::maybe-modnamelist-p (x) (declare (xargs :guard t)) (let ((__function__ 'sv::maybe-modnamelist-p)) (declare (ignorable __function__)) (if (atom x) t (and (or (sv::modname-p (car x)) (not (car x))) (sv::maybe-modnamelist-p (cdr x))))))
Theorem:
(defthm sv::maybe-modnamelist-p-of-cons (equal (sv::maybe-modnamelist-p (cons a b)) (and (or (not a) (sv::modname-p a)) (sv::maybe-modnamelist-p b))))