		Search-engine friendly clone of the ACL2 documentation.

Oprewrite

Vl-replicate-weirdint-bits

Generate n copies of a weird integer.

Signature
(vl-replicate-weirdint-bits n x) → new-bits
Arguments: n — How many copies to generate.
Guard (natp n).; x — The bits of the weirdint.
Guard (vl-bitlist-p x).
Returns: new-bits — Type (vl-bitlist-p new-bits).

Definitions and Theorems

Function: vl-replicate-weirdint-bits

(defun vl-replicate-weirdint-bits (n x)
  (declare (xargs :guard (and (natp n) (vl-bitlist-p x))))
  (let ((__function__ 'vl-replicate-weirdint-bits))
    (declare (ignorable __function__))
    (if (zp n)
        nil
      (append-without-guard (vl-bitlist-fix x)
                            (vl-replicate-weirdint-bits (- n 1)
                                                        x)))))

Theorem: vl-bitlist-p-of-vl-replicate-weirdint-bits

(defthm vl-bitlist-p-of-vl-replicate-weirdint-bits
  (b* ((new-bits (vl-replicate-weirdint-bits n x)))
    (vl-bitlist-p new-bits))
  :rule-classes :rewrite)

Theorem: len-of-vl-replicate-weirdint-bits

(defthm len-of-vl-replicate-weirdint-bits
  (equal (len (vl-replicate-weirdint-bits n x))
         (* (nfix n) (len x))))

Theorem: vl-replicate-weirdint-bits-of-nfix-n

(defthm vl-replicate-weirdint-bits-of-nfix-n
  (equal (vl-replicate-weirdint-bits (nfix n) x)
         (vl-replicate-weirdint-bits n x)))

Theorem: vl-replicate-weirdint-bits-nat-equiv-congruence-on-n

(defthm vl-replicate-weirdint-bits-nat-equiv-congruence-on-n
  (implies (acl2::nat-equiv n n-equiv)
           (equal (vl-replicate-weirdint-bits n x)
                  (vl-replicate-weirdint-bits n-equiv x)))
  :rule-classes :congruence)

Theorem: vl-replicate-weirdint-bits-of-vl-bitlist-fix-x

(defthm vl-replicate-weirdint-bits-of-vl-bitlist-fix-x
  (equal (vl-replicate-weirdint-bits n (vl-bitlist-fix x))
         (vl-replicate-weirdint-bits n x)))

Theorem: vl-replicate-weirdint-bits-vl-bitlist-equiv-congruence-on-x

(defthm vl-replicate-weirdint-bits-vl-bitlist-equiv-congruence-on-x
  (implies (vl-bitlist-equiv x x-equiv)
           (equal (vl-replicate-weirdint-bits n x)
                  (vl-replicate-weirdint-bits n x-equiv)))
  :rule-classes :congruence)