		Search-engine friendly clone of the ACL2 documentation.

Numeric-range-retrieval

Num-val-num-ranges

Set of numeric ranges in a numeric value notation.

Signature
(num-val-num-ranges numval) → ranges
Arguments: numval — Guard (num-val-p numval).
Returns: ranges — Type (num-range-setp ranges).

This is empty for a direct numeric value notation, and a singleton for a numeric range value notation.

Definitions and Theorems

Function: num-val-num-ranges

(defun num-val-num-ranges (numval)
  (declare (xargs :guard (num-val-p numval)))
  (let ((__function__ 'num-val-num-ranges))
    (declare (ignorable __function__))
    (num-val-case numval
                  :direct nil
                  :range (insert (make-num-range :base numval.base
                                                 :min numval.min
                                                 :max numval.max)
                                 nil))))

Theorem: num-range-setp-of-num-val-num-ranges

(defthm num-range-setp-of-num-val-num-ranges
  (b* ((ranges (num-val-num-ranges numval)))
    (num-range-setp ranges))
  :rule-classes :rewrite)

Theorem: num-val-num-ranges-of-num-val-fix-numval

(defthm num-val-num-ranges-of-num-val-fix-numval
  (equal (num-val-num-ranges (num-val-fix numval))
         (num-val-num-ranges numval)))

Theorem: num-val-num-ranges-num-val-equiv-congruence-on-numval

(defthm num-val-num-ranges-num-val-equiv-congruence-on-numval
  (implies (num-val-equiv numval numval-equiv)
           (equal (num-val-num-ranges numval)
                  (num-val-num-ranges numval-equiv)))
  :rule-classes :congruence)