		Search-engine friendly clone of the ACL2 documentation.

Utilities

Fast-alist-free-each-alist-val

Applies fast-alist-free to every value bound in the alist x.

Signature
(fast-alist-free-each-alist-val x) → *

Definitions and Theorems

Function: fast-alist-free-each-alist-val

(defun fast-alist-free-each-alist-val (x)
 (declare (xargs :guard t))
 (let ((__function__ 'fast-alist-free-each-alist-val))
  (declare (ignorable __function__))
  (mbe
     :logic nil
     :exec
     (cond ((atom x) nil)
           ((atom (car x))
            (fast-alist-free-each-alist-val (cdr x)))
           (t (prog2$ (fast-alist-free (cdar x))
                      (fast-alist-free-each-alist-val (cdr x))))))))