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