(vl-msb-replicate-bitlist n bits) appends
(vl-msb-replicate-bitlist n bits) → *
This is used for multiple concatenations, e.g.,
Function:
(defun vl-msb-replicate-bitlist (n bits) (declare (xargs :guard (and (natp n) (true-listp bits)))) (let ((__function__ 'vl-msb-replicate-bitlist)) (declare (ignorable __function__)) (if (zp n) nil (append bits (vl-msb-replicate-bitlist (- n 1) bits)))))
Theorem:
(defthm true-listp-of-vl-msb-replicate-bitlist (true-listp (vl-msb-replicate-bitlist n bits)) :rule-classes :type-prescription)
Theorem:
(defthm vl-emodwirelist-p-of-vl-msb-replicate-bitlist (implies (vl-emodwirelist-p bits) (vl-emodwirelist-p (vl-msb-replicate-bitlist n bits))))
Theorem:
(defthm len-of-vl-msb-replicate-bitlist (equal (len (vl-msb-replicate-bitlist n bits)) (* (nfix n) (len bits))))