		Search-engine friendly clone of the ACL2 documentation.

Outcomes

Tops-from-transform-outcomes

Signature
(tops-from-transform-outcomes outcomes) → l
Arguments: outcomes — Guard (outcome-listp outcomes).
Returns: l — Type (toplevel-listp l).

Definitions and Theorems

Function: tops-from-transform-outcomes

(defun tops-from-transform-outcomes (outcomes)
 (declare (xargs :guard (outcome-listp outcomes)))
 (let ((__function__ 'tops-from-transform-outcomes))
  (declare (ignorable __function__))
  (if (endp outcomes)
      nil
   (let ((r (tops-from-transform-outcomes (cdr outcomes))))
    (if
     (equal (outcome-kind (car outcomes))
            ':transformation-success)
     (append
          (outcome-transformation-success->toplevels (car outcomes))
          r)
     r)))))

Theorem: toplevel-listp-of-tops-from-transform-outcomes

(defthm toplevel-listp-of-tops-from-transform-outcomes
  (b* ((l (tops-from-transform-outcomes outcomes)))
    (toplevel-listp l))
  :rule-classes :rewrite)