		Search-engine friendly clone of the ACL2 documentation.

Svtv-doc

4vec-to-bitwise-chars

Signature
(4vec-to-bitwise-chars upper lower width) → chars
Arguments: upper — Guard (integerp upper).; lower — Guard (integerp lower).; width — Guard (natp width).
Returns: chars — Type (character-listp chars).

Definitions and Theorems

Function: 4vec-to-bitwise-chars

(defun 4vec-to-bitwise-chars (upper lower width)
  (declare (xargs :guard (and (integerp upper)
                              (integerp lower)
                              (natp width))))
  (let ((__function__ '4vec-to-bitwise-chars))
    (declare (ignorable __function__))
    (b* (((when (zp width)) nil)
         (width (1- width))
         (up (logbitp width upper))
         (low (logbitp width lower))
         (char (if up (if low #\1 #\x)
                 (if low #\z #\0))))
      (cons char
            (4vec-to-bitwise-chars upper lower width)))))

Theorem: character-listp-of-4vec-to-bitwise-chars

(defthm character-listp-of-4vec-to-bitwise-chars
  (b* ((chars (4vec-to-bitwise-chars upper lower width)))
    (character-listp chars))
  :rule-classes :rewrite)