		Search-engine friendly clone of the ACL2 documentation.

Bools->int

Convert a list of Booleans into an integer.

Signature
(bools->int x) → *
Arguments: x — Guard (boolean-listp x).

Produces a two's-complement integer from a list of bits, least-significant first. The last element of the list determines the sign of the value. Some examples:

(t) and (t t t) both evaluate to -1
nil, (nil), and (nil nil nil) all evaluate to 0
(t t t nil) evaluates to 7
(nil nil t) evaluates to -4.

Definitions and Theorems

Function: bools->int

(defun bools->int (x)
  (declare (xargs :guard (boolean-listp x)))
  (let ((__function__ 'bools->int))
    (declare (ignorable __function__))
    (mbe :logic
         (if (atom (cdr x))
             (- (bool->bit (car x)))
           (logcons (bool->bit (car x))
                    (bools->int (cdr x))))
         :exec (cond ((atom x) 0)
                     ((atom (cdr x)) (- (bool->bit (car x))))
                     (t (logcons (bool->bit (car x))
                                 (bools->int (cdr x))))))))

Theorem: bools->int-of-true-list-fix

(defthm bools->int-of-true-list-fix
  (equal (bools->int (true-list-fix x))
         (bools->int x)))

Theorem: bools->int-of-boolean-list-fix-x

(defthm bools->int-of-boolean-list-fix-x
  (equal (bools->int (acl2::boolean-list-fix x))
         (bools->int x)))

Theorem: bools->int-boolean-list-equiv-congruence-on-x

(defthm bools->int-boolean-list-equiv-congruence-on-x
  (implies (acl2::boolean-list-equiv x x-equiv)
           (equal (bools->int x)
                  (bools->int x-equiv)))
  :rule-classes :congruence)