		Search-engine friendly clone of the ACL2 documentation.

Range-tools

Vl-range-low-idx

Extract the lesser of the msb and lsb of a resolved vl-range.

Signature
(vl-range-low-idx x) → lowidx
Arguments: x — Guard (and (vl-range-p x) (vl-range-resolved-p x)).
Returns: lowidx — Type (integerp lowidx).

Definitions and Theorems

Function: vl-range-low-idx

(defun vl-range-low-idx (x)
  (declare (xargs :guard (and (vl-range-p x)
                              (vl-range-resolved-p x))))
  (let ((__function__ 'vl-range-low-idx))
    (declare (ignorable __function__))
    (min (vl-range-msbidx x)
         (vl-range-lsbidx x))))

Theorem: integerp-of-vl-range-low-idx

(defthm integerp-of-vl-range-low-idx
  (b* ((lowidx (vl-range-low-idx x)))
    (integerp lowidx))
  :rule-classes :type-prescription)