Generate the information and events for all the numeric ranges in a grammar.
(deftreeops-gen-all-numrange-infos+events rules prefix print) → (mv numrange-infos numrange-events event-alist)
Function:
(defun deftreeops-gen-all-numrange-infos+events (rules prefix print) (declare (xargs :guard (and (rulelistp rules) (common-lisp::symbolp prefix) (evmac-input-print-p print)))) (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 event-alist) (deftreeops-gen-numrange-alist-events infos prefix print)) (events (append get-nat-fn-events bounds-thm-events))) (mv infos events event-alist))))
Theorem:
(defthm deftreeops-numrange-info-alistp-of-deftreeops-gen-all-numrange-infos+events.numrange-infos (b* (((mv ?numrange-infos ?numrange-events ?event-alist) (deftreeops-gen-all-numrange-infos+events rules prefix print))) (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 ?event-alist) (deftreeops-gen-all-numrange-infos+events rules prefix print))) (pseudo-event-form-listp numrange-events)) :rule-classes :rewrite)
Theorem:
(defthm symbol-pseudoeventform-alistp-of-deftreeops-gen-all-numrange-infos+events.event-alist (b* (((mv ?numrange-infos ?numrange-events ?event-alist) (deftreeops-gen-all-numrange-infos+events rules prefix print))) (symbol-pseudoeventform-alistp event-alist)) :rule-classes :rewrite)