(collect-bits-bound-to-x keys alist) → *
Function:
(defun collect-bits-bound-to-x (keys alist) (declare (xargs :guard t)) (let ((__function__ 'collect-bits-bound-to-x)) (declare (ignorable __function__)) (b* (((when (atom keys)) nil) (lookup (hons-get (car keys) alist)) ((when (eq (cdr lookup) 'x)) (cons (car keys) (collect-bits-bound-to-x (cdr keys) alist)))) (collect-bits-bound-to-x (cdr keys) alist))))