		Search-engine friendly clone of the ACL2 documentation.

Stv-assemble-output-alist

Collect-bits-bound-to-x

Signature
(collect-bits-bound-to-x keys alist) → *

Definitions and Theorems

Function: collect-bits-bound-to-x

(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))))