		Search-engine friendly clone of the ACL2 documentation.

Append-alist-keys

Append-alist-keys-exec

Tail-recursive implementation of append-alist-keys.

This is used in the implementation of append-alist-keys. You should never need to reason about this -exec function directly, thanks to the following rule:

Theorem: append-alist-keys-exec-removal

(defthm append-alist-keys-exec-removal
        (equal (append-alist-keys-exec x acc)
               (revappend (append-alist-keys x) acc)))

Definitions and Theorems

Function: append-alist-keys-exec

(defun
 append-alist-keys-exec (x acc)
 (declare (xargs :guard t))
 (mbe
  :logic (if (atom x)
             acc
             (append-alist-keys-exec (cdr x)
                                     (revappend (caar x) acc)))
  :exec
  (cond
       ((atom x) acc)
       ((atom (car x))
        (append-alist-keys-exec (cdr x) acc))
       (t (append-alist-keys-exec (cdr x)
                                  (revappend-without-guard (caar x)
                                                           acc))))))