Generate the alist from numeric ranges to numeric range information, from a list of rules.
(deftreeops-gen-numrange-info-alist rules prefix) → infos
We obtain the set of numeric ranges from the rules, and then we generate an alist from the set.
Function:
(defun deftreeops-gen-numrange-info-alist-aux (ranges prefix) (declare (xargs :guard (and (num-range-setp ranges) (common-lisp::symbolp prefix)))) (let ((__function__ 'deftreeops-gen-numrange-info-alist-aux)) (declare (ignorable __function__)) (b* (((when (emptyp ranges)) nil) (range (head ranges)) (info (deftreeops-gen-numrange-info range prefix)) (infos (deftreeops-gen-numrange-info-alist-aux (tail ranges) prefix))) (acons range info infos))))
Theorem:
(defthm deftreeops-numrange-info-alistp-of-deftreeops-gen-numrange-info-alist-aux (implies (num-range-setp ranges) (b* ((infos (deftreeops-gen-numrange-info-alist-aux ranges prefix))) (deftreeops-numrange-info-alistp infos))) :rule-classes :rewrite)
Function:
(defun deftreeops-gen-numrange-info-alist (rules prefix) (declare (xargs :guard (and (rulelistp rules) (common-lisp::symbolp prefix)))) (let ((__function__ 'deftreeops-gen-numrange-info-alist)) (declare (ignorable __function__)) (deftreeops-gen-numrange-info-alist-aux (rulelist-num-ranges rules) prefix)))
Theorem:
(defthm deftreeops-numrange-info-alistp-of-deftreeops-gen-numrange-info-alist (b* ((infos (deftreeops-gen-numrange-info-alist rules prefix))) (deftreeops-numrange-info-alistp infos)) :rule-classes :rewrite)