		Search-engine friendly clone of the ACL2 documentation.

Svex-focused-equivalence-checking

A4veclist->upper-a4vecs-acc

Signature
(a4veclist->upper-a4vecs-acc x acc) → *
Arguments: x — Guard (a4veclist-p x).; acc — Guard (true-listp acc).

Definitions and Theorems

Function: a4veclist->upper-a4vecs-acc

(defun a4veclist->upper-a4vecs-acc (x acc)
  (declare (xargs :guard (and (a4veclist-p x) (true-listp acc))))
  (let ((__function__ 'a4veclist->upper-a4vecs-acc))
    (declare (ignorable __function__))
    (if (atom x)
        (reverse (llist-fix acc))
      (a4veclist->upper-a4vecs-acc
           (cdr x)
           (cons (b* ((upper (a4vec->upper (car x))))
                   (a4vec upper upper))
                 acc)))))