		Search-engine friendly clone of the ACL2 documentation.

Svex-focused-equivalence-checking

A4vec-accumulate-nodes

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

Definitions and Theorems

Function: a4vec-accumulate-nodes

(defun a4vec-accumulate-nodes (x acc)
  (declare (xargs :guard (a4vec-p x)))
  (let ((__function__ 'a4vec-accumulate-nodes))
    (declare (ignorable __function__))
    (b* (((a4vec x)))
      (hons-aiglist-accumulate-nodes
           x.upper
           (hons-aiglist-accumulate-nodes x.lower acc)))))