		Search-engine friendly clone of the ACL2 documentation.

Svex-focused-equivalence-checking

A4veclist-upper-subnodes

Signature
(a4veclist-upper-subnodes x) → *
Arguments: x — Guard (a4veclist-p x).

Definitions and Theorems

Function: a4veclist-upper-subnodes

(defun a4veclist-upper-subnodes (x)
  (declare (xargs :guard (a4veclist-p x)))
  (let ((__function__ 'a4veclist-upper-subnodes))
    (declare (ignorable __function__))
    (b* ((acc (a4veclist-accumulate-upper-nodes x nil)))
      (fast-alist-free acc)
      (mbe :logic (alist-keys acc)
           :exec (strip-cars acc)))))