Generate the information for a numeric range.
(deftreeops-gen-numrange-info range prefix) → info
Function:
(defun deftreeops-gen-numrange-info (range prefix) (declare (xargs :guard (and (num-range-p range) (common-lisp::symbolp prefix)))) (let ((__function__ 'deftreeops-gen-numrange-info)) (declare (ignorable __function__)) (b* (((num-range range) range) (range-part-of-name (num-base-case range.base :dec (str::cat "%D" (str::nat-to-dec-string range.min) "-" (str::nat-to-dec-string range.max)) :hex (str::cat "%X" (str::nat-to-hex-string range.min) "-" (str::nat-to-hex-string range.max)) :bin (str::cat "%B" (str::nat-to-bin-string range.min) "-" (str::nat-to-bin-string range.max)))) (get-nat-fn (packn-pos (list prefix '- range-part-of-name '-nat) prefix)) (bounds-thm (packn-pos (list get-nat-fn '-bounds) prefix))) (make-deftreeops-numrange-info :get-nat-fn get-nat-fn :bounds-thm bounds-thm))))
Theorem:
(defthm deftreeops-numrange-infop-of-deftreeops-gen-numrange-info (b* ((info (deftreeops-gen-numrange-info range prefix))) (deftreeops-numrange-infop info)) :rule-classes :rewrite)