(lit-list-for-levels x levels) → *
Function:
(defun lit-list-for-levels (x levels) (declare (xargs :stobjs (levels))) (declare (xargs :guard t)) (let ((__function__ 'lit-list-for-levels)) (declare (ignorable __function__)) (if (atom x) t (and (litp-for-levels (car x) levels) (lit-list-for-levels (cdr x) levels)))))