		Search-engine friendly clone of the ACL2 documentation.

Bvec

N2v

Convert a natural into a corresponding unsigned bvec (with constant bits).

Signature
(n2v n) → *

Definitions and Theorems

Function: n2v

(defun n2v (n)
  (declare (xargs :guard t))
  (let ((__function__ 'n2v))
    (declare (ignorable __function__))
    (if (eql (nfix n) 0)
        nil
      (bfr-ucons (equal 1 (logcar n))
                 (n2v (logcdr n))))))

Theorem: true-listp-of-n2v

(defthm true-listp-of-n2v
  (true-listp (n2v n))
  :rule-classes :type-prescription)

Theorem: bfr-list->u-of-n2v

(defthm bfr-list->u-of-n2v
  (equal (bfr-list->u (n2v n) env)
         (nfix n)))

Theorem: pbfr-list-depends-on-of-n2v

(defthm pbfr-list-depends-on-of-n2v
  (not (pbfr-list-depends-on k p (n2v n))))