		Search-engine friendly clone of the ACL2 documentation.

Range-tools

Vl-range-lsbidx

Extract the LSB (right) index from a resolved vl-range.

Signature
(vl-range-lsbidx x) → lsb
Arguments: x — Guard (and (vl-range-p x) (vl-range-resolved-p x)).
Returns: lsb — Type (integerp lsb).

Definitions and Theorems

Function: vl-range-lsbidx

(defun vl-range-lsbidx (x)
       (declare (xargs :guard (and (vl-range-p x)
                                   (vl-range-resolved-p x))))
       (let ((__function__ 'vl-range-lsbidx))
            (declare (ignorable __function__))
            (b* (((vl-range x) x))
                (vl-resolved->val x.lsb))))

Theorem: integerp-of-vl-range-lsbidx

(defthm integerp-of-vl-range-lsbidx
        (b* ((lsb (vl-range-lsbidx x)))
            (integerp lsb))
        :rule-classes :type-prescription)