		Search-engine friendly clone of the ACL2 documentation.

Oprewrite

Vl-replicate-constint-value

Generate n copies of a constant integer.

Signature
(vl-replicate-constint-value n width x) → replicated
Arguments: n — How many copies to generate.
Guard (natp n).; width — The bit-width of x.
Guard (posp width).; x — The integer to replicate.
Guard (natp x).
Returns: replicated — Type (natp replicated).

Definitions and Theorems

Function: vl-replicate-constint-value

(defun vl-replicate-constint-value (n width x)
  (declare (xargs :guard (and (natp n) (posp width) (natp x))))
  (let ((__function__ 'vl-replicate-constint-value))
    (declare (ignorable __function__))
    (let ((width (lposfix width)))
      (if (zp n)
          0
        (+ (ash (lnfix x) (* width (1- n)))
           (vl-replicate-constint-value (- n 1)
                                        width x))))))

Theorem: natp-of-vl-replicate-constint-value

(defthm natp-of-vl-replicate-constint-value
  (b* ((replicated (vl-replicate-constint-value n width x)))
    (natp replicated))
  :rule-classes :type-prescription)

Theorem: vl-replicate-constint-value-of-nfix-n

(defthm vl-replicate-constint-value-of-nfix-n
  (equal (vl-replicate-constint-value (nfix n)
                                      width x)
         (vl-replicate-constint-value n width x)))

Theorem: vl-replicate-constint-value-nat-equiv-congruence-on-n

(defthm vl-replicate-constint-value-nat-equiv-congruence-on-n
  (implies (acl2::nat-equiv n n-equiv)
           (equal (vl-replicate-constint-value n width x)
                  (vl-replicate-constint-value n-equiv width x)))
  :rule-classes :congruence)

Theorem: vl-replicate-constint-value-of-pos-fix-width

(defthm vl-replicate-constint-value-of-pos-fix-width
  (equal (vl-replicate-constint-value n (pos-fix width)
                                      x)
         (vl-replicate-constint-value n width x)))

Theorem: vl-replicate-constint-value-pos-equiv-congruence-on-width

(defthm vl-replicate-constint-value-pos-equiv-congruence-on-width
  (implies (acl2::pos-equiv width width-equiv)
           (equal (vl-replicate-constint-value n width x)
                  (vl-replicate-constint-value n width-equiv x)))
  :rule-classes :congruence)

Theorem: vl-replicate-constint-value-of-nfix-x

(defthm vl-replicate-constint-value-of-nfix-x
  (equal (vl-replicate-constint-value n width (nfix x))
         (vl-replicate-constint-value n width x)))

Theorem: vl-replicate-constint-value-nat-equiv-congruence-on-x

(defthm vl-replicate-constint-value-nat-equiv-congruence-on-x
  (implies (acl2::nat-equiv x x-equiv)
           (equal (vl-replicate-constint-value n width x)
                  (vl-replicate-constint-value n width x-equiv)))
  :rule-classes :congruence)