		Search-engine friendly clone of the ACL2 documentation.

Range-tools

Vl-maybe-range-lowidx

Extract the lesser of the msb and lsb of a resolved vl-maybe-range; treats the empty range as [0:0], i.e., its low index is 0.

Signature
(vl-maybe-range-lowidx 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-maybe-range-lowidx

(defun vl-maybe-range-lowidx (x)
  (declare (xargs :guard (and (vl-range-p x)
                              (vl-range-resolved-p x))))
  (let ((__function__ 'vl-maybe-range-lowidx))
    (declare (ignorable __function__))
    (if x (vl-range-msbidx x) 0)))

Theorem: integerp-of-vl-maybe-range-lowidx

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