		Search-engine friendly clone of the ACL2 documentation.

Svex-focused-equivalence-checking

A4veclist-accumulate-nodes

Signature
(a4veclist-accumulate-nodes x acc) → *
Arguments: x — Guard (a4veclist-p x).

Definitions and Theorems

Function: a4veclist-accumulate-nodes

(defun a4veclist-accumulate-nodes (x acc)
  (declare (xargs :guard (a4veclist-p x)))
  (let ((__function__ 'a4veclist-accumulate-nodes))
    (declare (ignorable __function__))
    (if (atom x)
        acc
      (a4veclist-accumulate-nodes
           (cdr x)
           (a4vec-accumulate-nodes (car x) acc)))))