Generate the information and events for all the character value notations in a grammar.
(deftreeops-gen-all-charval-infos+events rules prefix print) → (mv charval-infos charval-events event-alist)
Function:
(defun deftreeops-gen-all-charval-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-charval-infos+events)) (declare (ignorable __function__)) (b* ((infos (deftreeops-gen-charval-info-alist rules prefix)) ((mv leafterm-thm-events event-alist) (deftreeops-gen-charval-alist-events infos prefix print)) (events leafterm-thm-events)) (mv infos events event-alist))))
Theorem:
(defthm deftreeops-charval-info-alistp-of-deftreeops-gen-all-charval-infos+events.charval-infos (b* (((mv ?charval-infos ?charval-events ?event-alist) (deftreeops-gen-all-charval-infos+events rules prefix print))) (deftreeops-charval-info-alistp charval-infos)) :rule-classes :rewrite)
Theorem:
(defthm pseudo-event-form-listp-of-deftreeops-gen-all-charval-infos+events.charval-events (b* (((mv ?charval-infos ?charval-events ?event-alist) (deftreeops-gen-all-charval-infos+events rules prefix print))) (pseudo-event-form-listp charval-events)) :rule-classes :rewrite)
Theorem:
(defthm symbol-pseudoeventform-alistp-of-deftreeops-gen-all-charval-infos+events.event-alist (b* (((mv ?charval-infos ?charval-events ?event-alist) (deftreeops-gen-all-charval-infos+events rules prefix print))) (symbol-pseudoeventform-alistp event-alist)) :rule-classes :rewrite)