Generate the information and events for all the numeric ranges in a grammar.
(deftreeops-gen-all-numrange-infos+events rules prefix) → (mv numrange-infos numrange-events)
Function:
(defun deftreeops-gen-all-numrange-infos+events (rules prefix) (declare (xargs :guard (and (rulelistp rules) (common-lisp::symbolp prefix)))) (let ((__function__ 'deftreeops-gen-all-numrange-infos+events)) (declare (ignorable __function__)) (b* ((infos (deftreeops-gen-numrange-info-alist rules prefix)) ((mv get-nat-fn-events bounds-thm-events) (deftreeops-gen-numrange-alist-events infos prefix)) (events (append get-nat-fn-events bounds-thm-events))) (mv infos events))))
Theorem:
(defthm deftreeops-numrange-info-alistp-of-deftreeops-gen-all-numrange-infos+events.numrange-infos (b* (((mv ?numrange-infos ?numrange-events) (deftreeops-gen-all-numrange-infos+events rules prefix))) (deftreeops-numrange-info-alistp numrange-infos)) :rule-classes :rewrite)
Theorem:
(defthm pseudo-event-form-listp-of-deftreeops-gen-all-numrange-infos+events.numrange-events (b* (((mv ?numrange-infos ?numrange-events) (deftreeops-gen-all-numrange-infos+events rules prefix))) (pseudo-event-form-listp numrange-events)) :rule-classes :rewrite)