		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)