		Search-engine friendly clone of the ACL2 documentation.

Bvec

V2i

Convert a (pure constant) signed bvec into an integer.

Signature
(v2i v) → *
Arguments: v — Guard (true-listp v).

Definitions and Theorems

Function: v2i

(defun v2i (v)
  (declare (xargs :guard (true-listp v)))
  (let ((__function__ 'v2i))
    (declare (ignorable __function__))
    (mbe :logic
         (if (s-endp v)
             (bool->sign (car v))
           (logcons (bool->bit (car v))
                    (v2i (scdr v))))
         :exec
         (if (atom v)
             0
           (if (atom (cdr v))
               (if (car v) -1 0)
             (logcons (bool->bit (car v))
                      (v2i (cdr v))))))))

Theorem: v2i-of-bfr-eval-list

(defthm v2i-of-bfr-eval-list
  (equal (v2i (bfr-eval-list x env))
         (bfr-list->s x env)))

Theorem: v2i-of-i2v

(defthm v2i-of-i2v
  (equal (v2i (i2v x)) (ifix x)))