		Search-engine friendly clone of the ACL2 documentation.

Instant-runoff-voting

List-elements-equal

Returns t if all elements of x are equal to e

Signature
(list-elements-equal e x) → elem-equal?
Arguments: x — Guard (true-listp x).
Returns: elem-equal? — Type (booleanp elem-equal?).

Definitions and Theorems

Function: list-elements-equal

(defun list-elements-equal (e x)
  (declare (xargs :guard (true-listp x)))
  (let ((__function__ 'list-elements-equal))
    (declare (ignorable __function__))
    (if (endp x)
        t
      (and (equal (car x) e)
           (list-elements-equal e (cdr x))))))

Theorem: booleanp-of-list-elements-equal

(defthm booleanp-of-list-elements-equal
  (b* ((elem-equal? (list-elements-equal e x)))
    (booleanp elem-equal?))
  :rule-classes :type-prescription)