		Search-engine friendly clone of the ACL2 documentation.

4vec-operations

4v->4vec-bit

Convert a 4v-style ACL2::4vp into an infinite width 4vec of that bit.

Signature
(4v->4vec-bit x) → vec
Arguments: x — Guard (acl2::4vp x).
Returns: vec — Type (4vec-p vec).

Definitions and Theorems

Function: 4v->4vec-bit

(defun 4v->4vec-bit (x)
  (declare (xargs :guard (acl2::4vp x)))
  (let ((__function__ '4v->4vec-bit))
    (declare (ignorable __function__))
    (case x
      ((t) (2vec -1))
      ((f) (2vec 0))
      (z (4vec-z))
      (otherwise (4vec-x)))))

Theorem: 4vec-p-of-4v->4vec-bit

(defthm 4vec-p-of-4v->4vec-bit
  (b* ((vec (4v->4vec-bit x)))
    (4vec-p vec))
  :rule-classes :rewrite)