(vl-expr-arith-range-from-size/type x ss scopes) → (mv ok min max)
Function:
(defun vl-expr-arith-range-from-size/type (x ss scopes) (declare (xargs :guard (and (vl-expr-p x) (vl-scopestack-p ss) (vl-elabscopes-p scopes)))) (let ((__function__ 'vl-expr-arith-range-from-size/type)) (declare (ignorable __function__)) (b* (((mv ?warn size) (vl-expr-selfsize x ss scopes)) ((mv ?warn class) (vl-expr-typedecide x ss scopes)) ((unless (and size (vl-integer-arithclass-p class))) (mv nil 0 0))) (vl-arith-range-from-size/type size (vl-integer-arithclass->exprsign class)))))
Theorem:
(defthm integerp-of-vl-expr-arith-range-from-size/type.min (b* (((mv ?ok common-lisp::?min common-lisp::?max) (vl-expr-arith-range-from-size/type x ss scopes))) (integerp min)) :rule-classes :type-prescription)
Theorem:
(defthm integerp-of-vl-expr-arith-range-from-size/type.max (b* (((mv ?ok common-lisp::?min common-lisp::?max) (vl-expr-arith-range-from-size/type x ss scopes))) (integerp max)) :rule-classes :type-prescription)