		Search-engine friendly clone of the ACL2 documentation.

Vcd.lisp

Vcd-4vec-bitstr

Signature
(vcd-4vec-bitstr x width) → bits
Arguments: x — Guard (4vec-p x).; width — Guard (natp width).
Returns: bits — Type (stringp bits).

Definitions and Theorems

Function: vcd-4vec-bitstr

(defun vcd-4vec-bitstr (x width)
 (declare (xargs :guard (and (4vec-p x) (natp width))))
 (let ((__function__ 'vcd-4vec-bitstr))
  (declare (ignorable __function__))
  (b* (((4vec x) x))
   (vl-printedlist->string
        (vcd-print-4vec-aux x.upper x.lower
                            (min (lnfix width)
                                 (+ 1
                                    (max (integer-length x.upper)
                                         (integer-length x.lower))))
                            nil)))))

Theorem: stringp-of-vcd-4vec-bitstr

(defthm stringp-of-vcd-4vec-bitstr
  (b* ((bits (vcd-4vec-bitstr x width)))
    (stringp bits))
  :rule-classes :type-prescription)

Theorem: vcd-4vec-bitstr-of-4vec-fix-x

(defthm vcd-4vec-bitstr-of-4vec-fix-x
  (equal (vcd-4vec-bitstr (4vec-fix x) width)
         (vcd-4vec-bitstr x width)))

Theorem: vcd-4vec-bitstr-4vec-equiv-congruence-on-x

(defthm vcd-4vec-bitstr-4vec-equiv-congruence-on-x
  (implies (4vec-equiv x x-equiv)
           (equal (vcd-4vec-bitstr x width)
                  (vcd-4vec-bitstr x-equiv width)))
  :rule-classes :congruence)

Theorem: vcd-4vec-bitstr-of-nfix-width

(defthm vcd-4vec-bitstr-of-nfix-width
  (equal (vcd-4vec-bitstr x (nfix width))
         (vcd-4vec-bitstr x width)))

Theorem: vcd-4vec-bitstr-nat-equiv-congruence-on-width

(defthm vcd-4vec-bitstr-nat-equiv-congruence-on-width
  (implies (nat-equiv width width-equiv)
           (equal (vcd-4vec-bitstr x width)
                  (vcd-4vec-bitstr x width-equiv)))
  :rule-classes :congruence)