		Search-engine friendly clone of the ACL2 documentation.

Propagation-sigma

Remove-each-from-alist

BOZO, terrible, inefficient.

Signature
(remove-each-from-alist keys alist) → *

Definitions and Theorems

Function: remove-each-from-alist

(defun remove-each-from-alist (keys alist)
 (declare (xargs :guard (alistp alist)))
 (let ((__function__ 'remove-each-from-alist))
  (declare (ignorable __function__))
  (if (atom keys)
      alist
    (remove-each-from-alist (cdr keys)
                            (remove-from-alist (car keys) alist)))))

Theorem: vl-sigma-p-of-remove-from-alist

(defthm vl-sigma-p-of-remove-from-alist
  (implies (vl-sigma-p alist)
           (vl-sigma-p (remove-from-alist key alist))))

Theorem: vl-sigma-p-of-remove-each-from-alist

(defthm vl-sigma-p-of-remove-each-from-alist
  (implies (vl-sigma-p alist)
           (vl-sigma-p (remove-each-from-alist keys alist))))

Theorem: alistp-of-remove-each-from-alist

(defthm alistp-of-remove-each-from-alist
  (implies (alistp alist)
           (alistp (remove-each-from-alist keys alist))))