		Search-engine friendly clone of the ACL2 documentation.

Bvec

V2n

Convert an unsigned bvec into the corresponding natural.

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

Definitions and Theorems

Function: v2n

(defun v2n (v)
  (declare (xargs :guard (true-listp v)))
  (let ((__function__ 'v2n))
    (declare (ignorable __function__))
    (if (atom v)
        0
      (logcons (bool->bit (car v))
               (v2n (cdr v))))))

Theorem: v2n-of-bfr-eval-list

(defthm v2n-of-bfr-eval-list
  (equal (v2n (bfr-eval-list x env))
         (bfr-list->u x env)))

Theorem: v2n-of-n2v

(defthm v2n-of-n2v
  (equal (v2n (n2v x)) (nfix x)))