		Search-engine friendly clone of the ACL2 documentation.

Values

2vec

A 2vec is a 4vec that has no X or Z bits.

Signature
(2vec x) → *
Arguments: x — Guard (integerp x).

2vec constructs a 2vec from an integer; 2vec-p recognizes a 2vec; 2vec->val gets the integer value out of a 2vec.

Definitions and Theorems

Function: 2vec$inline

(defun 2vec$inline (x)
  (declare (xargs :guard (integerp x)))
  (let ((__function__ '2vec))
    (declare (ignorable __function__))
    (mbe :logic (4vec x x) :exec x)))

Theorem: 4vec-p-of-2vec

(defthm 4vec-p-of-2vec
  (4vec-p (2vec x)))

Theorem: 4vec->upper-of-2vec

(defthm 4vec->upper-of-2vec
  (equal (4vec->upper (2vec x)) (ifix x)))

Theorem: 4vec->lower-of-2vec

(defthm 4vec->lower-of-2vec
  (equal (4vec->lower (2vec x)) (ifix x)))

Theorem: equal-of-2vec

(defthm equal-of-2vec
  (equal (equal (2vec x) y)
         (and (4vec-p y)
              (equal (4vec->upper y) (ifix x))
              (equal (4vec->lower y) (ifix x)))))

Subtopics

2vec-p: Recognizer for 2vecs.
If-2vec-p: Helper macro for writing optimized 4vec-operations.
2vec->val: Extract the upper/lower value (both the same) from a 2vec.