		Search-engine friendly clone of the ACL2 documentation.

Bvec

Bfr-eval-list

Evaluate a list of BFRs, return the list of the (Boolean) results.

Signature
(bfr-eval-list x env) → bools
Returns: bools — Type (boolean-listp bools).

Definitions and Theorems

Function: bfr-eval-list

(defun bfr-eval-list (x env)
  (declare (xargs :guard t))
  (let ((__function__ 'bfr-eval-list))
    (declare (ignorable __function__))
    (if (atom x)
        nil
      (cons (bfr-eval (car x) env)
            (bfr-eval-list (cdr x) env)))))

Theorem: boolean-listp-of-bfr-eval-list

(defthm acl2::boolean-listp-of-bfr-eval-list
  (b* ((bools (bfr-eval-list x env)))
    (boolean-listp bools))
  :rule-classes :rewrite)

Theorem: bfr-eval-list-when-atom

(defthm bfr-eval-list-when-atom
  (implies (atom x)
           (equal (bfr-eval-list x env) nil)))

Theorem: bfr-eval-list-of-cons

(defthm bfr-eval-list-of-cons
  (equal (bfr-eval-list (cons a x) env)
         (cons (bfr-eval a env)
               (bfr-eval-list x env))))

Theorem: consp-of-bfr-eval-list

(defthm consp-of-bfr-eval-list
  (equal (consp (bfr-eval-list x env))
         (consp x)))

Theorem: bfr-eval-list-of-append

(defthm bfr-eval-list-of-append
  (equal (bfr-eval-list (append a b) env)
         (append (bfr-eval-list a env)
                 (bfr-eval-list b env))))

Theorem: boolean-list-bfr-eval-list

(defthm boolean-list-bfr-eval-list
  (implies (boolean-listp x)
           (equal (bfr-eval-list x env) x)))

Theorem: boolean-list-bfr-eval-list-const

(defthm boolean-list-bfr-eval-list-const
  (implies (and (syntaxp (quotep x))
                (boolean-listp x))
           (equal (bfr-eval-list x env) x)))

Theorem: bfr-eval-list-of-list-fix

(defthm bfr-eval-list-of-list-fix
  (equal (bfr-eval-list (list-fix x) env)
         (bfr-eval-list x env)))