		Search-engine friendly clone of the ACL2 documentation.

Vl-bit

Vl-bit->char

Convert a vl-bit-p into the corresponding character, e.g., #\0 or #\X.

Signature
(vl-bit->char x) → char
Arguments: x — Guard (vl-bit-p x).
Returns: char — Type (characterp char).

(vl-bit->char x) produces the ASCII character for a vl-bit-p. That is, it returns one of the characters: 0, 1, X, or Z.

Definitions and Theorems

Function: vl-bit->char

(defun vl-bit->char (x)
  (declare (xargs :guard (vl-bit-p x)))
  (let ((__function__ 'vl-bit->char))
    (declare (ignorable __function__))
    (let ((x (mbe :logic (vl-bit-fix x) :exec x)))
      (case x (:vl-0val #\0)
            (:vl-1val #\1)
            (:vl-xval #\X)
            (:vl-zval #\Z)
            (otherwise (progn$ (impossible) #\X))))))

Theorem: characterp-of-vl-bit->char

(defthm characterp-of-vl-bit->char
  (b* ((char (vl-bit->char x)))
    (characterp char))
  :rule-classes :type-prescription)

Theorem: vl-bit->char-of-vl-bit-fix-x

(defthm vl-bit->char-of-vl-bit-fix-x
  (equal (vl-bit->char (vl-bit-fix x))
         (vl-bit->char x)))

Theorem: vl-bit->char-vl-bit-equiv-congruence-on-x

(defthm vl-bit->char-vl-bit-equiv-congruence-on-x
  (implies (vl-bit-equiv x x-equiv)
           (equal (vl-bit->char x)
                  (vl-bit->char x-equiv)))
  :rule-classes :congruence)