(vl-lucid-range->bits x) → bits
Function:
(defun vl-lucid-range->bits (x) (declare (xargs :guard (vl-range-p x))) (declare (xargs :guard (vl-range-resolved-p x))) (let ((__function__ 'vl-lucid-range->bits)) (declare (ignorable __function__)) (b* (((vl-range x)) (msb (vl-resolved->val x.msb)) (lsb (vl-resolved->val x.lsb)) (min (min msb lsb)) (max (max msb lsb))) (nats-from min (+ 1 max)))))
Theorem:
(defthm return-type-of-vl-lucid-range->bits (b* ((bits (vl-lucid-range->bits x))) (and (nat-listp bits) (setp bits))) :rule-classes :rewrite)
Theorem:
(defthm vl-lucid-range->bits-of-vl-range-fix-x (equal (vl-lucid-range->bits (vl-range-fix x)) (vl-lucid-range->bits x)))
Theorem:
(defthm vl-lucid-range->bits-vl-range-equiv-congruence-on-x (implies (vl-range-equiv x x-equiv) (equal (vl-lucid-range->bits x) (vl-lucid-range->bits x-equiv))) :rule-classes :congruence)