		Search-engine friendly clone of the ACL2 documentation.

Bvec

I2v

Convert an integer into a corresponding signed bvec (with constant bits).

Signature
(i2v n) → *

Definitions and Theorems

Function: i2v

(defun i2v (n)
  (declare (xargs :guard t))
  (let ((__function__ 'i2v))
    (declare (ignorable __function__))
    (cond ((eql 0 (ifix n)) '(nil))
          ((eql n -1) '(t))
          (t (bfr-scons (equal (logcar n) 1)
                        (i2v (logcdr n)))))))

Theorem: bfr-list->s-of-i2v

(defthm bfr-list->s-of-i2v
  (equal (bfr-list->s (i2v n) env)
         (ifix n)))

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

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