		Search-engine friendly clone of the ACL2 documentation.

Bfr-eval-cp

Bfr-eval-vals

Signature
(bfr-eval-vals clause patterns) → *

Definitions and Theorems

Function: bfr-eval-vals

(defun bfr-eval-vals (clause patterns)
  (declare (xargs :guard t))
  (let ((__function__ 'bfr-eval-vals))
    (declare (ignorable __function__))
    (let ((collect (collect-bfr-eval-vals-list clause patterns)))
      (or collect '(arbitrary-vals)))))

Theorem: bfr-eval-vals-pseudo-term-listp

(defthm bfr-eval-vals-pseudo-term-listp
  (implies (pseudo-term-listp clause)
           (pseudo-term-listp (bfr-eval-vals clause patterns))))