(vl-nbits-fix n bits) → bits-fix
Function:
(defun vl-nbits-fix$inline (n bits) (declare (xargs :guard (and (posp n) (vl-bitlist-p bits)))) (declare (xargs :guard (equal (len bits) (pos-fix n)))) (let ((__function__ 'vl-nbits-fix)) (declare (ignorable __function__)) (mbe :logic (if (and (vl-bitlist-p bits) (equal (len bits) (pos-fix n))) bits (replicate (pos-fix n) :vl-xval)) :exec bits)))
Theorem:
(defthm vl-bitlist-p-of-vl-nbits-fix (b* ((bits-fix (vl-nbits-fix$inline n bits))) (vl-bitlist-p bits-fix)) :rule-classes :rewrite)
Theorem:
(defthm consp-of-vl-nbits-fix (consp (vl-nbits-fix n bits)) :rule-classes :type-prescription)
Theorem:
(defthm len-of-vl-nbits-fix (equal (len (vl-nbits-fix n bits)) (pos-fix n)))
Theorem:
(defthm vl-nbitsfix-identity (implies (and (vl-bitlist-p bits) (equal (len bits) (pos-fix n))) (equal (vl-nbits-fix n bits) bits)))
Theorem:
(defthm vl-nbits-fix-of-pos-fix (equal (vl-nbits-fix (pos-fix n) bits) (vl-nbits-fix n bits)))